Author name cluster

Mila Majster-Cederbaum

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

I&C Journal 2010 Journal Article

On hierarchically developing reactive systems

Naijun Zhan
Mila Majster-Cederbaum

The hierarchical development method is one of the most practical and effective methods for designing large reactive systems by allowing a design at different levels of abstraction. Combining hierarchical specification with hierarchical implementation plays a key role in decreasing the complexity of the verification of these systems. But, up to now, little work has been done related to the topic. In this paper, we investigate this issue.

Details DOI

TCS Journal 2004 Journal Article

Towards the hierarchical verification of reactive systems

Mila Majster-Cederbaum
Frank Salger

The hierarchical design approach for action based systems that is known as action refinement has been studied in the literature extensively. In a paper of M. Huhn published in CONCUR 1996 a refinement operator on a linear time logic is presented that mimics precisely a semantic action refinement on synchronisation structures. We present here an alternative approach where our starting point is a process algebraic setting with a syntactic action refinement. We present a refinement operator on the Modal Mu-calculus that conforms with the process algebraic refinement in the following sense: Provided some reasonable conditions are met, the transition system induced by a process term P satisfies a Modal Mu-Calculus-specification ϕ if and only if the system which is induced by a refinement of P satisfies a particular refinement of ϕ. Alleviating these conditions, we show that each of the two implications in the equivalence assertion above can be separately proven valid for a particular fragment of the Modal Mu-calculus. We demonstrate that the obtained results can indeed be used as a hierarchical verification technique. As a further application of our results, we explain how they can be employed as an abstraction technique in order to enhance model checking techniques.

Details DOI

TCS Journal 2000 Journal Article

Towards a unified view of bisimulation: a comparative study

Markus Roggenbach
Mila Majster-Cederbaum

The realm of approaches to operational descriptions and equivalences for concurrent systems in the literature lead to a series of different attempts to give a uniform characterization of what should be considered a bisimulation, mostly in an algebraic and/or categorical framework. Meanwhile the realm of such approaches calls itself for comparison and/or unification. We investigate how different abstract characterizations of bisimulations are related. In particular, we consider the coalgebraic approach of Aczel and Mendler, the observation structures (Kripke structures) of Degano, De Nicola and Montanari, the algebraic approach of Malacaria, the domain theoretic view of Abramsky and the categorical setting of Joyal, Nielsen and Winskel. The framework of Aczel and Mendler turns out to be the most general one in the sense that the other approaches can be translated into it. These translations, where the relation between the categorical setting of Joyal, Nielsen and Winskel with the coalgebraic approach is the most complicated one, enhance the understanding of the different approaches and contribute to a unified view of bisimulation.

Details DOI