Abstract
We study property preserving transformations for reactive systems. A key idea is the use of ϱ-simulations which are simulations parametrized by a relation ϱ, relating the domains of two systems. We particularly address the problem of property preserving abstractions of composed programs. For a very general notion of parallel composition, we give the conditions under which simulation is a precongruence for parallel composition and we study which kind of global properties are preserved by these abstractions.
This work was partially supported by ESPRIT Basic Research Actions “SPEC” and “REACT”.
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
M. Abadi and L. Lamport. The existence of refinement mappings. Technical Report SRC-29, DEC Research Center, 1988.
A. Bouajjani, S. Bensalem, C. Loiseaux, and J. Sifakis. Property preserving simulations. In Workshop on Computer-Aided Verification (CAV), Montréal, To appear in LNCS, june 1992.
J. A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. TCS, 37 (1), 1985.
R. E. Bryant. Graph based algorithms for boolean function manipulation. IEEE Trans. on Computation, 35 (8), 1986.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, january 1977.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Symposium on Principles of Programming Languages (POPL 92), ACM, october 1992.
K. M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, Massachusetts, 1988.
R. Cleaveland and B. Steifen. When is “partial” adequate? a logic-based proof technique using partial specifications. In LICS, 1990.
T. Filkorn. Functional extension of symbolic model checking. In Workshop on Computer-Aided Verification 91, Aalborg (Denmark), LNCS Vol. 575, june 1991.
O. Grumberg and E. Long. Compositionnal model checking and modular verification. In J.C.M. Baeten and J.F. Groote, editors, Concur '91, 2nd International Conference on Concurrency Theory, pages 250–265, Springer-Verlag, august 1991.
S. Graf and J. Sifakis. A logic for the specification and proof of regular controllable processes of CCS. Acta Informatica, 23, 1986.
Hubert Garavel and Joseph Sifakis. Compilation and verification of Lotos specifications. In L. Logrippo, R. L. Probert, and H. Ural, editors, Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa), IFIP, North Holland, Amsterdam, june 1990.
S. Graf and B. Steffen. Compositional minimisation of finite state processes. In Workshop on Computer-Aided Verification, Rutgers, LNCS 531, june 1990.
R.J. Van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). CS-R 8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989.
A.J. Hu, D.L. Dill, A.J. Drexler, and C.H. Yang. Higher-level specification and verification with bdds. In 4th Workshop on Computer-Aided Verification (CAV92), Montréal, To appear in LNCS, Springer Verlag, june 1992.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, 32:137–161, 1985.
C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall International, 1985.
ISO. IS ISO/OSI 8807-LOTOS: a formal description technique based on the temporal ordering of observational behaviour. International Standard, ISO, 1989.
J. Katzenelson and B. Kurshan. S/R: A Language for Specifying Protocols and other Coordinating Processes. In 5th Ann. Int'l Phoenix Conf. Comput. Commun., pages 286–292, IEEE, 1986.
D. Kozen. Results on the propositional μ-calculus. In Theoretical Computer Science, North-Holland, 1983.
R.P. Kurshan. Analysis of discrete event coordination. In REX Workshop on Stepwise Refinement of Distributed Systems, Mook, LNCS 430, Springer Verlag, 1989.
L. Lamport. The Temporal Logic of Actions. Technical Report 79, DEC, Systems Research Center, 1991.
K. G. Larsen and B. Thomsen. Compositional proofs by partial specification of processes. In LICS 88, 1988.
N.A. Lynch and M.R. Tuttle. An introduction to Input/Ouput Automata. MIT/LCS/TM 373, MIT, Cambridge, Massachussetts, november 1988.
R. Milner. An algebraic definition of simulation between programs. In Proc. Second Int. Joint Conf. on Artificial Intelligence, pages 481–489, BCS, 1971.
O. Ore. Galois connexions. Trans. Amer. Math. Soc, 55:493–513, February 1944.
G. Shurek and O. Grumberg. The Modular Framework of Computer-aided Verification: Motivation, Solutions and Evaluation Criteria. In Conference on Automatic Verification (CAV), Rutgers, NJ, LNCS 531, Springer Verlag, 1990.
D. J. Walker. Bisimulation and Divergence in CCS. In 3th Symposium on Logic in Computer Science (LICS 88), IEEE, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Graf, S., Loiseaux, C. (1993). Property preserving abstractions under parallel composition. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_95
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_95
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive