Abstract
MEC is a tool for constructing and analysing transition systems modelizing processes and systems of communicating processes.
From representations of processes by transition systems and from a representation of the interactions between the processes of a system by the set of all allowed global actions, MEC builds a transition system representing the global system of processes as the synchronized product of the component processes.
Such transition systems can be checked by computing sets of states and sets of transitions verifying properties given by the user of MEC. These properties are expressed in a language allowing definitions of new logical operators as least fixed points of systems of equations; thus all properties expressed in most of the branching-time temporal logic can be expressed in this language too.
MEC can handle transition systems with some hundred thousands states and transitions. Constructions of transition systems by synchronized products and computations of sets of states and transitions are performed in time linear with respect to the size of the transition system.
Unité de Recherche associée au Centre National de la Recherche Scientifique no 726
Work supported by the French Research Project C 3
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Arnold. Transition systems and concurrent processes. In Mathematical problems in Computation theory (Banach Center Publications,vol. 21), 1987.
A. Arnold and P. Crubillé. A linear algorithm to solve fixed point equations on transition systems. Inf. Process. Lett., 29:57–66, 1988.
A. Arnold and M. Nivat. Comportements de processus. In Colloque AFCET “Les Mathématiques de l'Informatique”, pages 35–68, 1982.
D. Bégay. Mode d'emploi MEC. Technical Report I-8915, Université Bordeaux I, 1989.
J. E. Burns. Symmetry in systems of asynchronous processes. In Proc. 22nd Annual Symp. on Foundations of Computer Science, pages 169–174, 1981.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logics specifications. ACM Trans. Prog. Lang. Syst., 8:244–263, 1986.
A. Dicky. An algebraic and algorithmic method for analysing transition systems. Theoretical Comput. Sci., 46:285–303, 1986.
E. A. Emerson and E. C. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In J. de Bakker and J. van Leeuwen, editors, 7th Int. Coll. on Automata, Languages and Programming, pages 169–181, Lect. Notes. Comput. Sci. 85, 1980.
E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Symp. on Logic in Comput. Sci., pages 267–278, 1986.
R. M. Keller. Formal verification of parallel programs. Commun. ACM, 19:371–384, 1976.
D. Kozen. Results on the propositional μ-calculus. Theoretical Comput. Sci., 27:333–354, 1983.
M. Nivat. Sur la synchronisation des processus. Revue Technique Thomson-CSF, 11:899–919, 1979.
V. Pratt. A decidable μ-calculus. In Proc. 22nd Symp. on Foundations of Comput. Sci., pages 421–427, 1981.
J.-P. Queille. Le système CESAR: Description, spécification et analyse des applications réparties. PhD thesis, I.N.P., Grenoble, 1982.
J. Sifakis. Global and local invariants in transition systems. Technical Report 274, IMAG, Grenoble, 1981.
R. E. Tarjan. Depth first search and linear graph algorithms. SIAM J. Comput., 1:146–160, 1972.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arnold, A. (1990). MEC : a system for constructing and analysing transition systems. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_11
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive