computer science

Research Interests of Irek Ulidowski

My research is in Concurrency, and concerns semantics of and specification formalisms for concurrent systems within the operational style originated by Plotkin and Milner. The aim is to unify and generalise the theories for particular process languages, for example CCS and CSP, into meta-theories for classes of process languages, where a class is determined by a format (a set of syntactic forms) of Plotkin-style Structural Operational Semantics (SOS) rules in which its process operators are defined.

I researched the following topics.

1. General formats of SOS rules and congruence results for these formats.
2. Process preorders and equivalences on processes where silent actions are abstracted away and divergence plays a crucial role.
3. Algorithms for generation of sound and complete proof systems for process languages defined by a format of SOS rules and for a process equivalence.
4. Extensions of general process languages (defined by a format of SOS rules) with discrete time.
5. Algorithms for generation of Priority Rewrite Systems for OSOS process languages defined by the OSOS format and for strong bisimulation.
6. Reversing computation in algebraic process languages.

Below, I describe the results of my work in more detail. Firstly, a brief explanation of SOS rules, formats of rules and the role of congruence results.

Each SOS (transition) rule has the following form.

The conclusion of a rule describes the behaviour of a process constructed with an operator and several components, and the premises describe the behaviour of the components. Process operators, and hence PLs, can be classified according to the format of their SOS rules. One can associate a class of PLs with a format: the class consists of all those PLs whose operators are definable in the format. It is traditional to work with well-behaved formats, namely those formats that preserve the chosen process equivalence, in other words those formats for which the chosen equivalence is a congruence. The congruence results for an equivalence and a format guarantee compositionality of specification and reasoning with respect to the equivalence within any process language in the format.

The details of the results follow:

1. General formats of SOS rules and the congruence results for them.
   • The ISOS format is developed in LICS92 and my PhD thesis. It offers an intuitive treatment of silent actions, negative premises (inability to perform actions in stable states) and copying (multiple use of process variables). All ISOS definable process operators preserve eager bisimulation preorder, a divergence sensitive version of weak bisimulation preorder (PhD thesis). They also preserve refusal simulation preorder (PhD thesis), a generalisation of ready simulation of Bloom.
   • The De Simone format with silent actions is studied in my PhD thesis and in CONCUR95, AMAST96 and TCS2000. It is a sub-format of the ISOS format, where rules have no negative premises and no copying. It is proved in TCS2000 that testing preorder of De Nicola and Hennessy is preserved by all De Simone operators.
   • The Ordered SOS (OSOS) format is presented in TAPSOFT97 and IC2002 papers. The format employs positive GSOS rules equipped with orderings. This new feature allows one to control the order of application of rules when deriving transitions of process terms. We show that the OSOS format has the same expressive power as the GSOS format, and that strong bisimulation is preserved by the OSOS format.
   • The ebo and bbo formats are studied in TAPSOFT97 and IC2002 papers. These formats are subformats of the OSOS format; they provide an intuitive and safe treatment of silent actions, copying and divergence. We prove that ebo and bbo operators preserve eager bisimulation and branching bisimulation preorders respectively.
   • The rebo and rbbo formats, and several interesting subformats, are studied in CONCUR2000 paper. These formats preserve the rooted versions of eager and branching bisimulation preorders respectively. All widely used process operators are definable in these formats.
2. Process preorders and equivalences based on testing are considered in LICS92, PhD thesis, AMAST96, TCS2000 and TAPSOFT97 papers. I studied the whole range of tests including traces, refusals, acceptances, copying and global tests. I identified a class of tests, represented by copy+refusal tests, which are sufficiently powerful to distinguish between processes with a different finite and local behaviour. The preorder based on copy+refusal tests, copy+refusal preorder ( LICS92, PhD thesis), has a number of intuitive and natural characterisations in terms of
   • ISOS and ebo trace precongrunce ( LICS92, PhD thesis, TAPSOFT97 )
   • refusal simulation preorder ( LICS92, PhD thesis),
   • preorder based on Limited Modal Logic (PhD thesis) (a version of Hennessy Milner Logic).
3. Algorithms for generation of sound and complete axiomatisations for De Simone process languages and
   • refusal simulation preorder ( CONCUR95),
   • testing preorder of De Nicola and Hennessy ( AMAST96 and TCS2000)

   The algorithm in CONCUR95 can be easily adjusted to produce axiomatisations for coarser preorders than refusal simulation preorder, for example refusal or ready trace preorders.

4. Extensions of process languages with time: AMAST97 and JLAP2004. We propose a uniform framework, based on the Ordered SOS approach, for extending arbitrary process languages with discrete time. The framework guarantees that a timed version of rooted eager bisimulation preorder is preserved the extended process language, as well as all processes satisfy the time determinacy and maximal time synchrony properties.

   Our framework allows the user to select the most suitable timed process language for a task in hand. This is possible because the user can choose any operators, whether they are standard or new application-specific operators, provided that they can be defined in the framework. We also propose several constraints on OSOS rules for the operators such that some other timed properties, for example the maximal progress and weak timelock freeness, are satisfied.

5. Algorithms for generation of Priority Rewrite Systems for OSOS process languages and strong bisimulation: CONCUR2003. A link between automatic generation of complete axiomatisations and automatic generation of term rewrite systems for a process language is intriguing. I have developed a procedure that produces terminating and confluent rewrite systems for a subclass of GSOS process languages.

   Priority Rewrite Systems (PRS) of Baeten, Bergstra, Klop and Weijland are rewrite systems with a priority ordering on the rewrite rules. I have developed an algorithm that generates a PRS for a given OSOS process language. For each OSOS operator, the algorithm produces a set of `oriented' axioms, that are to be used form left to right, together with a precedence ordering on the oriented axioms derived from the ordering on the rules. I have identified a subclass of OSOS process languages such that the generated PRSs enjoy confluence, and termination properties.

6. Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, and even programming languages for quantum computing. We developed a procedure for converting operators of standard algebraic process calculi such as CCS, ACP and CSP into reversible operators, while preserving their operational semantics. We define a forward-reverse bisimulation and prove that it is a congruence for all reversible operators.

© University of Leicester. Last modified: 6th November 2005, 07:12:23
CS Web Maintainer. Any opinions expressed on this page are those of the author.