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.
General formats of SOS rules and congruence results for these formats.
Process preorders and equivalences on processes where silent actions are
abstracted away and divergence plays a crucial role.
Algorithms for generation of sound and complete proof systems for process languages
defined by a format of SOS rules and for a process equivalence.
Extensions of general process languages (defined by a format of SOS rules) with
discrete time.
Algorithms for generation of Priority Rewrite Systems for OSOS
process languages defined by the OSOS format and for strong bisimulation.
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.
premises
-------------
conclusion
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:
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.
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
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.
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.
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.
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.