Research

ATYlogo

Research interests

  1. Structured Operational Semantics
  2. (Timed) Process Algebra
  3. Verification of Timed Systems
  4. Hybrid Systems
  5. Message Sequence Charts
Structured Operational Semantics

In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS’s) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues.

Structural Operational Semantics [G.D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming 60 (2004) 17–139] has become the common way to define operational semantics. Operational semantics defines the possible transitions that a piece of syntax can make during its “execution”. Each transition may be labelled by a message to be communicated to the outside world. Transitions of a composed piece of syntax can usually be defined in a generic way, in terms of the transitions of its constituent parts. This forms the central idea behind Structural Operational Semantics (SOS).

Soon after its introduction, and due to its popularity, SOS itself became a subject of study, thus resulting in “SOS meta-theory” and “SOS rule formats”. The first SOS meta-result dates back to the Ph.D. Thesis of Robert de Simone [R. de Simone, Calculabilit´e et expressivit´e dans l’alg`ebre de processus parall`eles Meije, Th`ese de 3e cycle, Univ. Paris 7, 1984] (in French), an excerpt of which appeared in 1985 [R. de Simone, Higher-level synchronizing devices in MEIJE-SCCS, Theoretical Computer Science 37 (1985) 245–267].

Transition System Specifications (TSS’s), as introduced by Groote and Vaandrager in [J.F. Groote, F.W. Vaandrager, Structured operational semantics and bisimulation as a congruence, Information and Computation 100 (2) (1992) 202–260], are a formalization of SOS. By imposing syntactic restrictions on TSS’s one can deduce several interesting properties about their induced operational semantics. These properties range from well-definedness of the operational semantics to security- and probability-related issues. The syntactic restrictions imposed by these meta-theorems usually suggest particular forms of deduction rules to be safe for a particular purpose and hence these meta-theorems usually define what is called a rule format.

The above description is adapted from [M.R. Mousavi, M.A. Reniers and J.F. Groote. SOS Formats and Meta-Theory: 20 Years After. Theoretical Computer Science, 373(3):238-272, April 200].

Key publications in this research area are
  1. M.R. Mousavi, M.A. Reniers and J.F. Groote. SOS Formats and Meta-Theory: 20 Years After. Theoretical Computer Science, 373(3):238-272, April 2007.
  2. M.R. Mousavi, M.A. Reniers and J.F. Groote. Notions of Bisimulation and Congruence Formats for SOS with Data. Information & Computation, 200(1):107-147, 2005.
  3. MohammadReza Mousavi, Iain Phillips, M.A. Reniers, and Irek Ulidowski. Semantics and Expressiveness of Ordered SOS. Information and Computation, 207:85-119, March 3, 2009.
  4. Sjoerd Cranen, MohammadReza Mousavi, and Michel A. Reniers. A Rule Format for Associativity. In Franck van Breugel and Marsha Chechik, editors, CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008, pages 447-461. Lecture Notes in Computer Science, volume 5201, Springer, 2008.
  5. D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda and R.R.H. Schiffelers. Syntax and Consistent Equation Semantics of Hybrid Chi. Journal of Logic and Algebraic Programming, 68(1-2):129-210, June-July 2006.
(Timed) Process Algebra

Key publications in this research area are

  1. J.C.M. Basten, T. Basten, and M.A. Reniers. Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, September 2009.
  2. J.F. Groote and M.A. Reniers. Algebraic Process Verification In J.A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra. Chapter 17, pages 1151-1208, Elsevier Science B.V., March 2001.
  3. P.J.L. Cuijpers and M.A. Reniers. Hybrid Process Algebra. Journal of Logic and Algebraic Programming, 62(2):191-245. February 2005.
  4. M.A. Reniers, J.F. Groote, M.B. van der Zwaag, and J. van Wamel. Completeness of Timed mCRL. Fundamenta Informaticae, 50(3-4):361-402, April-May 2002.
  5. J.C.M. Baeten and M.A. Reniers. Duplication of Constants in Process Algebra. Journal of Logic and Algebraic Programming, 70(2):151-171, February 2007.

Verification of Timed Systems

Key publications in this research area are

  1. K. Klai, L. Petrucci, and M.A. Reniers. An Incremental and Modular Technique for checking LTL\X properties of Petri nets. In J. Derrick and J. Vain, editors, Proceedings of 27th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2007), Tallinn, Estonia, June 27-29, 2007, pages 280-295. Lecture Notes in Computer Science, Vol. 4574, 2007, Springer.
  2. J.J.T. Kleijn, M.A. Reniers and J.E. Rooda. Analysis of an Industrial System. Formal Methods in System Design, 22(3):249-282, May 2003.
  3. Jan Friso Groote, Michel A. Reniers, and Yaroslav S. Usenko. Verification of Networks of Timed Automata using mCRL2. In 22nd IEEE International Symposium on Parallel and Distributed Processing (IPDPS 2008), Miami, Florida, USA. April 14-18, 2008, pages 1-8. IEEE
  4. J.F. Groote, M.A. Reniers and Y.S. Usenko. Time Abstraction in Timed mCRL à la Regions. 20th International Parallel and Distributed Processing Symposium 2006 (IPDPS'06). Island of Rhodes, Greece, April 25-26, 2006.
  5. S.H.J. Bos and M.A. Reniers. The I2C-bus in Discrete-Time Process Algebra. Science of Computer Programming, 29(1-2):235-258, 1997.

Hybrid Systems

Key publications in this research area are

  1. Hybrid Process Algebra. Journal of Logic and Algebraic Programming, 62(2):191-245. February 2005.
  2. P.C.W. van den Brand, M.A. Reniers and P.J.L. Cuijpers. Linearization of Hybrid Processes. Journal of Logic and Algebraic Programming, 68(1-2):54-104, June-July 2006. Special issue on Process Theory for Hybrid Systems.
  3. D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda and R.R.H. Schiffelers. Syntax and Consistent Equation Semantics of Hybrid Chi. Journal of Logic and Algebraic Programming, 68(1-2):129-210, June-July 2006.
  4. D.A. van Beek, M.A. Reniers, R.R.H. Schiffelers and J.E. Rooda. Foundations of a Compositional Interchange Format for Hybrid Systems. In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, 10th International Conference on Hybrid Systems: Computation and Control (HSCC'07), April 3-5 2007, Pisa, Italy, pages 587-600. Lecture Notes in Computer Science, volume 4416, 2007, Springer.
  5. P.J.L. Cuijpers and M.A. Reniers. Lost in Translation: Hybrid-Time Flows vs. Real-Time Transitions. In M. Egerstedt and B. Mishra, editors, 11th International Conference on Hybrid Systems: Computation and Control (HSCC'08), St. Louis, USA, April 22-24, 2008, pages 116–129. Lecture Notes in Computer Science, volume 4981, Springer, 2008.

Message Sequence Charts

Key publications in this research area are

  1. S. Mauw and M.A. Reniers. An algebraic semantics of Basic Message Sequence Charts. The Computer Journal, 37(4):269-277, 1994.
  2. A.G. Engels, S. Mauw and M.A. Reniers. A hierarchy of communication models for Message Sequence Charts. Science of Computer Programming, 44(3):253-292, September 2002.
  3. S. Mauw and M.A. Reniers. Operational Semantics for MSC'96. Computer Networks and ISDN Systems, 31(17):1785-1799, 1999. Elsevier Science B.V.
  4. S. Mauw and M.A. Reniers. High-Level Message Sequence Charts. In A. Cavalli and A. Sarma, editors, SDL'97: Time for Testing - SDL, MSC and Trends, Proceedings of the Eighth SDL Forum, Evry, France, 23-26 September, 1997, pages 291-306.
  5. M.A. Reniers. Message Sequence Chart: Syntax and Semantics. PhD Thesis, Eindhoven University of Technology, June 1999.

Program committee

  1. Member of Programme Committee SOS 2009: Workshop on Structured Operational Semantics, Bologna, Italy, August 31, 2009.
  2. Member of Programme Committee SOS 2008: Workshop on Structured Operational Semantics, Reykjavik, Iceland, July 6, 2008.
  3. Member of Organizing Committee of FMICS 1998, Amsterdam, The Netherlands, May 25-16, 1998.