User Tools

Site Tools


This is an old revision of the document!

Home page of Michel Reniers ( M.A. Reniers)


Please visit for a personal homepage of me.


Under development

Some of the topics I am currently working on are listed below:

  • Symbolic SOS for CIF 2.0

The Structured Operational Semantics of languages such as (Hybrid) Chi and CIF 2.0 result in infinite transition systems. One of the reasons of infinity can be that there are many solutions to a differential equation or to a predicate describing an update of the model variables. Another reason for infinity is in the way flow transitions are generated with different durations.

In this research we try to replace the concrete SOS by a symbolic SOS in which the values of the model variables are not incorporated yet in the semantics. It is our goal to obtain a finite symbolic transition system that may be instantiated to deliver the concrete transition system by incorporating appropriate valuations of model variables. We study the possibilities to base the development of a simulator for CIF 2.0 on such a symbolic SOS. Other (sub-)lines of research in this subject are

  • Model Checking Behavioural Properties on Symbolic SOS
  • Applicability of SOS meta-theory on Symbolic SOS for obtaining properties of the concrete SOS

First experiments indicate that indeed it is possible to give a Symbolic SOS for the language CIF 2.0 (without scope operators). A formal relationship is established between the original concrete SOS and the new Symbolic SOS. As soon as these results are published this will be mentioned here.

  • Hybrid Process Algebra

We are developing a succesor for the modelling languages Chi (Chi 1) and Hybrid Chi (Chi 2). The language should allow for the combined specification of both discrete-event and continuous-time behaviour of systems. In due time, a simulator for this language will be developed. We are also considering to apply verification technology to models given in this language. On the technical side, we feel that the language should be a conservative extension of the basic process algbras from the book Process Algebra: Equational Theories of Communicating Processes by J.C.M. Baeten, T. Basten and M.A. Reniers.

  • Type Checking CIF 2.0

We try to specify type checking for CIF 2.0 expressions by means of a deduction system in Modular SOS. Ultimately, we strive to generate an implementation of a type checker based on such a specification.

  • Nominal SOS


Under development


Under development

Key Publications

  1. J.C.M. Baeten, T. Basten, and M.A. Reniers. Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, September 2009.
  2. P.J.L. Cuijpers and M.A. Reniers. Hybrid Process Algebra. Journal of Logic and Algebraic Programming, 62(2):191-245. February 2005.
  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. 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.


* 4B050 Werktuigbouwkunde in Vogelvlucht

mreniers/start.1458948420.txt.gz · Last modified: Saturday, 26 March 2016 : 00:27:00 by mreniers