Abstract
We present a formalism to handle finite state concurrent systems in a mechanical way. In such a formalism we can axiomatically define concurrent systems by means of a branching time language. We show that, starting from the axiomatic description of a concurrent system, we can obtain automatically a finite Kripke model H such that theorem proving is reduced to model checking with respect to H. By means of such a formal procedure, we can model a large class of concurrent systems including Petri nets, CSP, Interaction Systems and so on. A tool has been implemented to produce a Kripke model from an axiomatical description of a concurrent system and to perform model checking on it.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
4. References
Ben-Ari, M., Pnueli, A. and Manna, Z., The temporal logic of branching time, Acta Informatica 20 (1983) 207–226.
Clarke, E.M., Emerson, E.A. and Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. Prog. Lang. Syst. 8 (1986) 244–263.
Emerson, E.A. and Clarke, E.M., Using branching time temporal logic to synthesize synchronization skeletons, Sci. Comp. Program. 2(1982) 241–266.
Emerson, E.A. and Lei, C.L., Modalities for model checking: Branching time strikes back, Proc. 12th Ann. Symp. Principles of Programming Languages, ACM, New York, 1985, 84–96.
Masini, A. and Maggiolo-Schettini, A., Local and global time logic: A formalism to describe finite-state distributed systems. Technical Report TR-5/88, Dipartimento di Informatica, Università di Pisa, 1988.
Manna, Z. and Wolper, P., Synthesis of communicating process from temporal logic specifications, ACM Trans. Prog. Lang. Syst. 6(1984) 68–93.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danelutto, M., Masini, A. (1989). A temporal logic approach to specify and to prove properties of finite state concurrent systems. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '88. CSL 1988. Lecture Notes in Computer Science, vol 385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026295
Download citation
DOI: https://doi.org/10.1007/BFb0026295
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51659-0
Online ISBN: 978-3-540-46736-6
eBook Packages: Springer Book Archive