Abstract
The paper addresses the specification of reactive behaviour for event-based models. We are concerned with a framework for such specification rather than with a particular style of specifications. Our main observation is that a logic of events is needed as well as a logic of actions. The former prescribes in fine detail how computations proceed while the latter provides generic scripts for events to happen. The analogy is that of procedures and procedure calls at runtime (= events). We claim that both logics are inherently interrelated, in particular, if “true concurrency” is to be specified.
In order to specify reactive behaviours we propose a logic of actions on top of a new model called event automata, focusing on the ingredients that such a specification method should provide.
Work partially supported by the German Ministry for Science and Technology, Verbundprojekt KORSO, subproject “Design of Reliable Reactive Systems” (grant No. ITS 900 1A7).
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brown, C., Gurr, D., “Temporal Logic and Categories of Petri Nets”, to appear
Costa, J.F., Sernadas, A., Sernadas, C., “The Semantics of Object-Oriented Specification”, in Proc. of the IS-Core '92 Workshop, INESC, Lisboa, 1992
Fiadeiro, J., Sernadas, A., Logics of Modal Terms for System Specification, Journal of Logics and Computation, Nordwijkerhout, 1990
Gunawardena, J., “Geometric logic, Causality and Event Structures”, in CONCUR'91, Lecture Notes in Computer Science 527, 1991, pp. 266–280
Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall, 1984
Hopcroft, J.E., Ullman, J.D., Introduction to Automata Theory, Languages and Computation, Addison Wesley, 1979
Mazurkiewicz, A., “Basic Notions of Trace Theory”, in Lecture Notes for the REX Summerschool in Temporal Logic, Lecture Notes in Computer Science 354, Springer, 1988
Milner, R., Communication and Concurrency, Prentice Hall, 1989
Olderog, E.-R., Hoare, C.A.R., Specification-oriented Semantics for Communicating Processes, Acta Informatica 23, pp. 9–66
Petri, C.A., Kommunikation mit Automaten, Institut für Instrumentelle Mathematik, Schriften des IIM, Nr. 2, Bonn 1962 also: Griffiths Air Force Base, Techn. Rep. RADC-TR-65-377, Vol.1, Suppl.1 (English translation), New York, 1966
Petri, C.A., “Concurrency”, in Net Theory and Applications, Lecture Notes in Computer Science 84, Springer, 1979
Pinna, G.M., Poigné, A., “On the Nature of Events”, in Proc. MFCS'92, Lecture Notes in Computer Science 629, 1992, pp. 430–441
Pinna, G.M., Poigné, A., “On the Nature of Events”, GMD-Arbeitspapier, to appear
Pinna, G.M., Poigné, A., The Mathematics of Event Automata, in preparation
Manna, Z., Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems Specification, Springer, 1992
Pratt, V., “Modeling Concurrency with Partial Orders”, International Journal of Parallel Programming, Vol.15, 1986
Rensink, A., “Posets for Configurations!”, in CONCUR'92, Lecture Notes in Computer Sciences 630, pp. 269–285
Winskel, G., “Event Structures”, in Petri Nets: Applications and Relationships to other Models of Concurrency, Lecture Notes in Computer Sciences 255, pp. 325–392
Winskel, G., Categories of Models for Concurrency, Talk at ESPRIT-BRA CLICS-Meeting, Paris, 1990
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pinna, G.M., Poigné, A. (1994). On the specification of elementary reactive behaviour. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1993. Lecture Notes in Computer Science, vol 802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58027-1_13
Download citation
DOI: https://doi.org/10.1007/3-540-58027-1_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58027-0
Online ISBN: 978-3-540-48419-6
eBook Packages: Springer Book Archive