• Journal papers
• Books
• Conference contributions
• Workshop contributions

 

Journal papers

Metric semantics for true concurrent real time.
J-P. Katoen, C. Baier, D. Latella.

 
This paper investigates the use of a complete metric space framework for providing denotational semantics to a  real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures,  a variant of Winskel's event structures. The distance function of the metric is based on the amount of time  to which event structures do `agree'.  We show that this intuitive notion of distance is a pseudo metric  (but not a metric) on the set of timed event structures.  A generalisation to equivalence classes of timed event structures  in which we abstract from event identities and non-executable events  (events that can never occur) is shown to be a complete  ultra-metric space.  We present an operational semantics for the considered  language and show that the metric semantics is an abstraction of it.  The operational semantics is characterised by the absence of synchronisation on the advance of time as opposed to the operational semantics of most real-time calculi.  The consistency between our metric and an existing  cpo-based denotational semantics is briefly investigated.

Theoretical Computer Science, vol. 254 no. 1/2, pages 501-542, 2001.

Process algebra for performance evaluation.
H. Hermanns, U. Herzog, J-P. Katoen.

 
This paper surveys the theoretical developments in the field of stochastic process algebras, process algebras where action occurrences may be subject to a delay that is determined by a random variable.  A huge class of resource-sharing systems - like large-scale computers, client-server architectures, networks - can accurately be described using such stochastic specification formalisms.

The main emphasis of this paper is the treatment of operational semantics, notions of equivalence, and (sound and complete) axiomatisations of these equivalences for different types of Markovian process algebras, where delays are governed by exponential distributions.  Starting from a simple action-less algebra for describing time-homogeneous continuous-time Markov chains, we consider the integration of actions and random delays both as a single entity (like in known Markovian process algebras like TIPP, PEPA and EMPA) and as separate entities (like in the timed process algebras timed CSP and TCCS).  In total we consider four related calculi and investigate their relationship to existing Markovian process algebras.  We also briefly indicate how one can profit from the separation of time and actions when incorporation more general, non-Markovian distributions.

Theoretical Computer Science, 2001 (to appear).

Pattern-matching algorithms based on term rewrite systems
J-P. Katoen, A. Nymeyer.

 
Automatic code generators often contain pattern matchers that are based on tree grammars. In this work we generalise this approach by developing pattern matchers that are based on more powerful term rewrite systems. A pattern matcher based on a term rewrite system computes all the sequences of rewrite rules that will reduce a given expression tree to a given goal. While the number of sequences of rewrite rules that are generated is typically enormous, the vast majority of sequences are in fact redundant. This redundancy is caused by the fact that many rewrite sequences are permutations of each other. A theory and a series of algorithms are systematically developed that identify and remove two types of redundant rewrite sequences. These algorithms terminate if rewrite sequences do not diverge.

Theoretical Computer Science, vol. 238 no. 1/2, pages 439-464, 2000.

Automated compositional Markov chain generation for a plain-old telephone system.
H. Hermanns, J-P. Katoen.

Obtaining performance models, like Markov chains and queueing networks, for systems of significant complexity and magnitude is a difficult task that is usually tackled using human intelligence and experience. This holds in particular for performance models of a highly irregular nature.  In this paper we argue by means of a non-trivial example --- a plain-old telephone system (POTS) --- that a stochastic extension of process algebra can diminish these problems by permitting an automatic generation of Markov chains. We introduce a stochastic process algebra that separates the advance  of time and action occurrences.  For the sake of specification convenience we incorporate an elapse operator that allows the modular description of time constraints where delays are described by continuous phase-type distributions.  Using this language we provide a formal specification of the POTS and show how a stochastic process of more than 10$^7$ states is automatically obtained from this system description.  Finally, we aggregate this model compositionally using appropriate stochastic extensions of (strong and weak) bisimulation.  As a result we obtain a highly irregular Markov chain of about 700 states in an automated way, which we use to carry out a transient performance analysis of the POTS.

Science of Computer Programming, vol. 36 no. 1, pages 97-127, 2000.  Full paper.

On generative parallel composition.
P. R. D'Argenio, H. Hermanns, J-P. Katoen.

A major reason for studying probabilistic processes is to establish a linkbetween a formal model for describing functional system behaviour and a stochastic process.  Compositionality is an essential ingredient for specifying systems.  Parallel composition in a probabilistic setting is complicated since it gives rise to non-determinism, for instance due to interleaving of independent autonomous activities.  This paper presents a detailed study of the resolution of non-determinism in an asynchronous generative setting.  Based on the intuition behind the synchronous probabilistic calculus PCCS we formulate two criteria that an asynchronous parallel composition should fulfill.  We provide novel probabilistic variants of parallel composition for CCS and CSP and show that these operators satisfy these general criteria, opposed to most existing proposals.  Probabilistic bisimulation is shown to be  congruence for these operators and their expansion is addressed.

Electronic Notes in Theoretical Computer Science, vol. 22, 1999. Full paper.

Automatic verification of a lip-synchronisation protocol using UPPAAL.
H. Bowman, G. Faconti, J-P. Katoen, D. Latella, M. Massink.

We present the formal specification and verification of a lip-synchronisation protocol using the real-time model checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some flaws in the protocol. In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error state.  We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis.

Formal Aspects of Computing, vol. 10, pages 550-575, 1998.  Full paper.

A consistent causality-based view on a timed process algebra including urgent interactions.
J-P. Katoen, E. Brinksma, R. Langerak, D. Latella, T. Bolognesi.

This paper discusses a timed variant of a process algebra akin to  LOTOS, baptized UPA, in a causality-based setting.  Two timed features are incorporated---a delay function which constrains the occurrence time of atomic actions and an urgency operator that forces (local or synchronized) actions to happen urgently.  Timeouts are typical urgent phenomena.  A novel timed  extension of event structures is introduced and used as a vehicle to provide a denotational causality-based semantics for UPA.  Recursion is dealt with by using standard fixpoint theory.  In addition, an operational semantics is  presented based on separate time- and action-transitions that is shown to be  consistent with the event structure semantics.  An interleaving semantics for UPA is immediately obtained from the operational semantics.  By adopting this dual approach the well-developed timed  interleaving view is extended with a consistent timed partial order view and a comparison is facilitated of the partial order model and the variety of  existing (interleaved) timed process algebras.

Journal of Formal Methods in System Design, vol. 12 no. 2, pages 189-216, 1998.

Partial-order models for quantitative extensions of LOTOS.
E. Brinksma, J-P. Katoen, R. Langerak, D. Latella.

Event structures are a prominent model for non-interleaving concurrency.  The use of event structures for providing a compositional  non-interleaving semantics to LOTOS without data is studied. In particular, several quantitative extensions of event structures are proposed that incorporate notions like time ---both of deterministic and stochastic nature--- and probability.   The suitability of these models for giving a non-interleaving semantics  to a timed, stochastic and probabilistic extension of LOTOS is investigated.  Consistency between the event structure semantics and an (event-based) operational semantics is addressed for the different quantitative variants of LOTOS and is worked out for the timed case in more detail.  These consistency results facilitate the coherent use of an interleaving and a non-interleaving semantic view in a single design trajectory and  provide a justification for the event structure semantics.  As a running example an infinite buffer is used in which gradually  timing constraints on latency and rates of accepting and producing  data and the probability of loss of messages are incorporated.

Computer Networks and ISDN Systems, vol. 30 no. 9/10, pages 925-950, 1998. Technical report 4/97.

Code generation based on formal BURS theory and heuristic search.
A. Nymeyer, J-P. Katoen.

BURS theory provides a powerful mechanism to efficiently generate pattern matches in a given expression tree.  BURS, which stands for bottom-up rewrite system, is based on term rewrite systems, to which costs are added.  We formalise the underlying theory, and derive an algorithm that computes all pattern matches.  This algorithm terminates if the term rewrite system is finite.  We couple this algorithm with the well-known search algorithm A* that carries out pattern selection.  The search algorithm is directed by a cost heuristic that estimates the minimum cost of code that has to be generated.  The advantage of using a search algorithm is that we need to compute only thoe costs that may be part of an optimal rewrite sequence (and not the costs of all possible rewrite sequences as in dynamic programming).  A system that implements the algorithms presented in this work has been built.

Acta Informatica, vol. 34 no. 8, pages 597-635, 1997. Full paper.

Design and analysis of dynamic leader election protocols in broadcast networks.
J.J. Brunekreef, J-P. Katoen, R.L.C. Koymans, S. Mauw.

The well-known problem of leader election in distributed systems is considered in a dynamic context where processes may participate and crash spontaneously.  Processes communicate by means of buffered broadcasting as opposed to usual  point-to-point communication. In this paper we design a leader election protocol  in such a dynamic context. As the problem at hand is considerably complex we  develop the protocol in three steps. In the initial design processes are considered to be perfect and a leader is assumed to be present initially. In the second protocol, the assumption of an initial leader is dropped. This leads to a symmetric protocol which uses an (abstract) timeout mechanism to detect the absence of a leader. Finally, in the last step design processes may crash without giving any notification ot other processes.  The worst case message complexity of all protocols is addressed.

A formal approach to the specification and verification of the leader election  protocols is adopted. The requirements are specified in a property-oriented way  and the protocols are denoted by means of extended finite state machines.  It is proven using linear-time temporal logic that the fault-tolerant  protocol satisfies its requirements.

Distributed Computing, vol. 9 no. 4, pages 157-171, 1996. Full paper.

Systolic arrays for the recognition of permutation-invariant segments.
J-P. Katoen, B. Schoenmakers.

Let P be a permutation defined on sequences of length N. A sequence of N values is said to be P-invariant when it does not change when permuted according to P.   A program is said to recognize P-invariant segments when it determines for each segment of N successive input values  whether it is P-invariant.

In this paper we derive a program scheme that generates efficient parallel programs for the recognition of P-invariant segments. The programs consist of a chain of cells extended with a linear number of links between non-neighbouring cells. Under reasonable conditions on P, these programs correspond to systolic arrays with both constant response time and constant latency (independent of N).  Efficient systolic arrays for problems such as palindrome recognition or perfect shuffle recognition can be constructed automatically in this way. This is illustrated for the palindrome recognition problem.

Science of Computer Programming, vol. 27 no. 2, pages 119-137, 1996. Full paper.

A stochastic causality-based process algebra.
E. Brinksma, J-P. Katoen, R. Langerak, D. Latella.

This paper discusses stochastic extensions of a simple process algebra in a causality-based setting.  Atomic actions are supposed to happen after a delay that is determined by a stochastic variable with a certain distribution.  A simple stochastic type of event structures is discussed, restricting the distribution functions to be exponential. A corresponding operational  semantics of this model is given and compared to existing (interleaved) approaches.  Secondly, a stochastic variant of event structures is discussed where distributions are of a much more general nature, viz.\of phase-type.  This includes exponential, Erlang, Coxian and mixtures of exponential distributions.

The Computer Journal, vol. 38 no. 7, pages 552-565, 1995. Full paper.

A design model for open distributed processing systems.
M. van Sinderen, L. Ferreira Pires, C.A. Vissers, J-P. Katoen.

This paper proposes design concepts that allow the conception, understanding and development of complex technical structures for open distributed systems.  The proposed concepts are related to, and partially motivated by, the present work on Open Distributed Processing (ODP).  As opposed to the current ODP approach, the concepts are aimed at supporting a design trajectory with several, related abstraction levels.  Simple eexamples are used to illustrate the proposed concepts.

Computer Networks and ISDN Systems, vol. 27 no. 6, pages 1263-1285, 1995.  Full paper (in pdf).

Recognizing K-rotated segments.
J-P. Katoen, M. Rem.

This paper explains a calculational design technique for fine-grained parallel  programs by means of an example. The example deals with the recognition of K-rotation invariant (or K-rotated) segments which is a generalisation of the  well-known square recognition problem.   Two parallel programs are derived. The first one determines for each segment of  N successive inputs whether it is K-rotated, the latter determines whether  the whole sequence thus far received is K-rotated.

International Journal of High Speed Computing, vol. 5 no. 2, pages 293-305, 1993. Full paper.

Bottom-up tree acceptors.
C. Hemerik, J-P. Katoen.

This paper deals with the formal derivation of an efficient tabulation algorithm for table-driven bottom-up tree acceptors.  Bottom-up tree acceptors are based on a notion of match sets.  First we derive a naive acceptance algorithm using dynamic computation of match sets.   Tabulation of match sets leads to an efficient acceptance algorithm, but tables may be so large that they can not be generated due to lack of space.   Introduction of a convenient equivalence relation on match sets reduces this effect and improves the tabulation algorithm.

Science of Computer Programming, vol. 13 no. 1, pages 51-72, 1990. Technical report.

Books

Formal Methods for Real-Time and Probabilistic Systems.
J-P. Katoen (editor).

No abstract available.

Proceedings ARTS'99, LNCS 1601, © Springer-Verlag, 1999.  How to order.
Online version (via Springer LINK).

Concepts, Algorithms and Tools for Model Checking.
J-P. Katoen.

No abstract available.

Arbeitsberichte der Informatik, Friedrich-Alexander-Universitaet Erlangen-Nuernberg, 292 pages, vol. 32 no. 1, Gruner Druck GmbH, 1999.

Qualitative and Quantitative Extensions of Event Structures.
J-P. Katoen.

No abstract available.

Ph.D thesis, University of Twente, 1996. Full document.

Conference contributions

First passage time analysis of stochastic process algebra using partial orders.
T.C. Ruys, R. Langerak, J-P. Katoen, D. Latella, M. Massink.

 
This paper proposes a partial-order semantics for a stochastic process algebra that supports general (non-memoryless) distributions and combines this with an approach to numerically analyse the first passage time of an event. Based on an adaptation of McMillan's complete finite prefix approach tailored to event structures and process algebra, finite representations are obtained for recursive processes. The behaviour between two events is now captured by a partial order that is mapped on a stochastic task graph, a structure amenable to numerical analysis. Our approach is supported by the (new) tool FOREST for generating the complete prefix and the (existing) tool PEPP for analysing the generated task graph. As a case study, the delay of the first resolution in the root contention phase of the IEEE 1394 serial bus protocol is analysed.

Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), LNCS xxxx, pages ?, © Springer-Verlag, 2001. Full paper.

On the use of model checking for quantitative dependability evaluation.
B. Haverkort, H. Hermanns, J-P. Katoen

 
Over the last two decades many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained fairly cumbersome. In this paper we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way.  Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process.
Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.

19th IEEE Symposium on Reliable Distributed Systems (SRDS), pages 228-238, © IEEE Computer Society Press, 2000.

Towards model checking stochastic process algebra.
H. Hermanns, J-P. Katoen, J. Meyer-Kayser, M. Siegle

 
Stochastic process algebras have been proven useful because they allow behaviour-oriented performance and reliability modelling.  As opposed to traditional performance modelling techniques, the behaviour-oriented style supports composition and abstraction in a natural way.  However, the analysis of stochastic process algebra models is state-oriented, beacuse standard numerical analysis is typically based on the calculation of (transient and steady) state probabilities.  This shift of paradigms hampers the acceptance of the process algebraic approach by performance modellers.  In this paper, we develop an entirely behaviour-oriented analysis technique for stochastic process algebras.  The key contribution is an action-based temporal logic to describe behaviours-of-interest, together with a model checking algorithm to derive the probability with which a stochastic process algebra model exhibits a given behaviour-of-interest.

Integrated Formal Methods (IFM 2000), LNCS 1945, pages 420-440, © Springer-Verlag, 2000.

On a temporal logic for object-based systems.
D. Distefano, J-P. Katoen, A. Rensink.

 
This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the specification of dynamic and static properties of object-based systems. The logic is based on the branching temporal logic CTL and the Object Constraint Language (OCL), an optional part of the UML standard for expressing static properties over class diagrams. The formal semantics of BOTL is defined in terms of a general operational model that is aimed to be applicable to a wide range of object-oriented languages. A mapping of a large fragment of OCL onto BOTL is defined, thus providing a formal semantics to OCL.

Formal Methods for Open Object-based Distributed Systems IV (FMOODS 2000), pages 305-326, ©Kluwer Academic Publishers, 2000. Full paper.

On the logical characterisation of performability properties.
C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen.

 
Markov-reward models, as extensions of continuous-time Markov chains, have received increased attention for the specification and evaluation of performance and dependability properties of systems. Until now, however, the specification of reward-based performance and dependability measures has been done manually and informally. In this paper, we change this undesirable situation by the introduction of a continuous-time, reward-based stochastic logic. We argue that this logic is adequate for expressing performability measures of a large variety. We isolate two important sub-logics, the logic CSL [ASS+96,BKH99], and the novel logic CRL that allows one to express reward-based properties. These logics turn out to be complementary, which is formally established in our main duality theorem. This result implies that reward-based properties expressed in CRL for a particular Markov reward model can be interpreted as CSL properties over a derived continuous-time Markov chain, so that model checking procedures for CSL can be employed.

Automata, Languages and Programming (ICALP 2000), LNCS 1853, pages 780-792, © Springer-Verlag, 2000. Full paper.

Model checking continuous-time Markov chains by transient analysis.
C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen.

 
The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [ASS+96,BaKH99], a stochastic branching-time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties over paths. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.

Computer-Aided Verification (CAV 2000), LNCS 1855, pages 358-372, © Springer-Verlag, 2000. Full paper.

A Markov chain model checker.
H. Hermanns, J-P. Katoen, J. Meyer-Kayser, M. Siegle.

 
Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete and the continuous time setting. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen--Twente Markov Chain Checker (ETMCC), where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of ETMCC.

Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), LNCS 1785, pages 347-362, © Springer-Verlag, 2000. Full paper.

Specification and analysis of soft real-time systems: quantity and quality.
P.R. D'Argenio, J-P. Katoen, E. Brinksma.

 
This paper presents a process algebra for specifying soft real-time constraints in a compositional way.  For these soft constraints we take a stochastic point of view and allow arbitrary probability distributions to express delays of activities.  The semantics of this process algebra is given in terms of stochastic automata, a variant of timed automata where clocks are initialised randomly and run backwards.  To analyse quantitative properties, an algorithm is presented for the on-the-fly generation of a discrete-event simulation model from a process algebra specification.  On the qualitative side, a symbolic technique for classical reachability analysis of stochastic automata is presented.  As a result a unifying framework for the specification and analysis of quantitative and qualitative properties is obtained.  We discuss an implementation of both analytic methods and specify and analyse a fault-tolerant multi-processor system.

IEEE Real-Time Systems Symposium (RTSS'99), pages 104-114, IEEE Computer Society Press, 1999. Full paper.

Approximate symbolic model checking of continuous-time Markov chains.
C. Baier, J-P. Katoen, H. Hermanns.

This paper presents a symbolic model checking algorithm for continuous-time Markov chains for an extension of the continuous stochastic logic CSL of Aziz et al.  The considered logic contains a time-bounded until-operator and a novel operator to express steady-state probabilities.  We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady state-operator) and a Volterra integral equation system for time-bounded until.  We propose a symbolic approximate method for solving the integrals using MTDDs (multi-terminal decision diagrams), a generalisation of MTBDDs.  These new structures are suitable for numerical integration using quadrature formulas based on equally-spaced abscissas, like trapezoidal, Simpson and Romberg integration schemes.

Concurrency Theory (CONCUR'99), LNCS 1664, pages 146-162, © Springer-Verlag, 1999.  Full paper.

Metric semantics for true concurrent real time.
C. Baier, J-P. Katoen, D. Latella.

This paper investigates the use of a complete metric space framework for providing denotational semantics to a  real-time process algebra.  The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures.  The distance function is based on the amount of time to which  event structures do `agree'.  We show that this intuitive notion of distance is a pseudo metric  (but not a metric) on the set of timed event structures.  A generalisation to equivalence classes of timed event structures  in which we abstract from event names and non-executable events (events that can never appear) is shown to be a complete ultra-metric space.  We show that the resulting metric semantics is an abstraction of an existing cpo-based denotational and a related operational  semantics for the considered language.

Automata, Languages and Programming (ICALP'98), LNCS 1443, pages 568-580, © Springer-Verlag, 1998. Full paper.

A true concurrency semantics for ET-LOTOS.
H. Bowman, J-P. Katoen.

 
One of the central objectives of the LOTOS restandardisation activity is to define an enhanced LOTOS language which supports  real-time specification.  The timed extension is based upon a timed LOTOS proposal ET-LOTOS.  This paper defines a (branching-time) non-interleaving semantics for ET-LOTOS without data.  As a denotational model a suitable timed extension of Langerak's bundle event structures is used.  For guarded recursive processes we show the consistency between our non-interleaving semantics and the ET-LOTOS interleaving semantics.  Since our semantical model does not have an explicit notion of the passage of time (as opposed to the interleaving semantics) we are able to handle unguarded recursion and Zeno-behaviours in a perspicuous way.

Applications of Concurrency to System Design (ACSD'98), pages 228-239, IEEE Computer Society Press, 1998. Full paper. (Extended abstract of Technical report IMMD VII-12/97. )

An algebraic approach to the specification of stochastic systems (extended abstract).
P. R. D'Argenio, J-P. Katoen, E. Brinksma.

We introduce a framework to study stochastic systems, i.e. systems in which the time of occurrence of activities is a general random variable.  We introduce and discuss in depth a stochastic process algebra (named SPADES) which is adequate to specify and analyse those systems.  In order to give semantics to SPADES, we also introduce a model that is an extension of traditional automata with clocks which are basically random variables: the stochastic automata model.  We show that this model and SPADES are equally expressive.  Although stochastic automata are adequate to analyse systems since they are finite objects, they are still too coarse to serve as concrete semantic objects.  Therefore, we introduce a type of probabilistic transition system that can deal with arbitrary probability spaces.  In addition, we give a finite axiomatisation for SPADES that is sound for the several semantic notions we deal with, and complete for the finest of them.  Moreover, an expansion law is straightforwardly derived.

Programming Concepts and Methods (PROCOMET'98), pages 126-148, North-Holland, 1998. Full paper.

Causal ambiguity and partial orders in event structures.
R. Langerak, E. Brinksma, J-P. Katoen.

Event structure models often have some constraint which ensures that for each system run it is clear what are the causal predecessors of an event (i.e., there is no causal ambiguity).   In this contribution we study what happens if we remove such constraints.  We define five different partial order semantics that are intentional in the sense that they refer to syntactic aspects of the model.  We also define an observational partial order semantics, that derives a partial order from just the event traces.

It appears that this corresponds to the so-called early intentional semantics;  the other intentional semantics cannot be observationally characterized. We study the equivalences induced by the different partial order definitions, and their interrelations.

Concurrency Theory (CONCUR'97), LNCS 1243, pages 317-332, © Springer-Verlag, 1997. Full paper.

The bounded retransmission protocol needs to be on time!
P.R. D'Argenio, J-P. Katoen, T. Ruys, G.J. Tretmans.

This paper concerns the transfer of files via a lossy communication channel.  It formally specifies this file transfer service in a property-oriented way and investigates---using two different techniques---whether a given bounded retransmission protocol conforms to this service.  This protocol is based on the well-known alternating bit protocol but allows for a bounded number of
retransmissions of a chunk, i.e., part of a file, only.  So, eventual delivery is not guaranteed and the protocol may abort the file transfer.  We investigate to what extent real-time aspects are important to guarantee the protocol's  correctness and use SPIN and UPPAAL model checking for our  purpose.

Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), LNCS 1217, pages 416-432, © Springer-Verlag, 1997. Full paper.More info.

The systematic development of a pattern-matching algorithm using term rewrite systems.
J-P. Katoen, A. Nymeyer.

A term rewrite system is used to specify a pattern matcher in a code generator.  The pattern matcher derived from the term rewrite system computes all sequences of rewrite rules that will reduce a given expression tree into a given goal.  While the number of sequences of rewrite rules that are generated is typically enormous, many sequences are in fact redundant.  A theory and  accompanying algorithms are developed that identify and remove these redundant rewrite sequences.  These algorithms terminate if the term rewrite system is finite.

Australian Computer Science Communications (CATS'97), vol. 19 no. 2, pages 59-71, 1997. Full paper.

Code generation = A* + BURS.
A. Nymeyer, J-P. Katoen, Y. Westra, H. Alblas.

A system called BURS that is based on term rewrite systems and a search algorithm A* are combined to produce a code generator that generates optimal code.  The theory underlying BURS is re-developed, formalised, and explained in this work.  The search algorithm uses a cost heuristic that is derived from the term rewrite system to direct the search.  The advantage of using a search algorithm is that we need to compute only those costss that may be part of an optimal rewrite sequence.

Compiler Construction (CC'96), LNCS 1060, pages 160-177, 1996. Full paper.

On specifying real-time systems in a causality-based setting.
J-P. Katoen, R. Langerak, D. Latella, E. Brinksma.

Event structures are a prominent noninterleaving model for concurrency.  Real-time event structures associate a set of time instants to events, modelling absolute time constraints, and to causal dependencies, modelling relative delays between causally dependent events. We introduce this novel temporal model and show how it can be used to provide a denotational  semantics to a real-time variant of a process algebra akin to LOTOS.  This formalism includes a timed-action prefix which constrains the occurrence time  of actions, a timeout and watchdog (i.e., timed interrupt) operator. An event-based operational semantics for this formalism is presented that is shown to be consistent with the denotational semantics.  As an example we use an infinite buffer with time constraints on the message latency and the rates of accepting and producing data.

Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'96), LNCS 1135, pages 385-405, © Springer-Verlag, 1996. Full paper.

B-ISDN to the cell site switch versus B-ISDN to the mobile terminal.
G. Karagiannis, J-P. Katoen, I.G.M.M. Niemegeers.

This paper addresses in detail two possible scenarios for integrating the future mobile telecommunication system UMTS with the evolving broadband fixed telecommunication system B-ISDN.  In the first scenario a mobile-specific access network is envisaged combined with a B-ISDN backbone network.  The second scenario uses B-ISDN basic call  facilities throughout the entire network, including the mobile access part. The two scenarios are described in detail and a comparison at functional level is made.  This comparison is complemented by a performance study of a non-trivial handover procedure in a high-traffic public environment.

Proceedings IEEE Int. Conference on Communicating Systems (ICCS'96), pages 629-633, IEEE Press, 1996. Full paper.

Causal behaviours and nets.
J-P. Katoen.

Specification formalisms in which causality and independence of actions can be explicitly expressed are beneficial from a design point of view.  The explicit presence (or absence) of a causal dependency between actions can be used effectively during the design.  We consider a specification formalism in which causal relations between actions play a central role and provide a  semantics in terms of (an extension of) labelled place/transition nets. The  behaviour of nets is defined by labelled partially ordered sets.

Application and Theory of Petri Nets (ATPN'95),LNCS 935, pages 258-277, © Springer-Verlag, 1995. Full paper.

Functional integration of B-ISDN and UMTS.
J-P. Katoen.

Nowadays mobile telecommunication systems and fixed  telecommunication  networks are developed as stand-alone systems and exist as separate and independent systems, interconnected at just a few points. A main objective of third generation mobile systems is to specify mobile-specific functionality as integral part of fixed networks. This paper addresses  the (possible) integration of future mobile and fixed systems, UMTS and B-ISDN. It proposes the use of advanced broadband basic call functions for  the support of mobile call setup and handover, addresses the common use of a communication infrastructure, and finally, investigates the support of handover by B-ISDN multi-party call capabilities.

Proceedings 45th IEEE Vehicular Technology Conference vol. 1 (VTC'95), IEEE Press, pages 163-168, 1995. Full paper.

Modelling systems by probabilistic process algebra: an event structures approach.
J-P. Katoen, R. Langerak, D. Latella.

Performance and reliability analysis of distributed systems based on formal specifications is an important and widely recognized issue. This paper treats a probabilistic version of (a subset of) the process algebra LOTOS.  It incorporates a probabilistic choice assigning a probability of occurrence to each of its alternatives.  Opposed to the traditional interleaving semantics used for existing probabilistic process algebras the presented language is based on a true concurrency semantics.  This enables us to distinguish between  non-determinism and parallelism, to reduce the state explosion problem and, moreover, to analyse part of the system without considering other (irrelevant) parts.  In this paper the language is presented and the formal semantics is defined by using an extension of bundle event structures.  A short example illustrates the novelties of the language and  links the language to stochastic analysis based on semi-Markov chains.

Formal Description Techniques (FORTE'93), IFIP Transactions C-22, pages 253-268, North-Holland, 1994. Full paper.

A semi-Markov model of a home network access protocol.
J-P. Katoen.

Home networks provide a means for interconnecting consumer products in home environments.  In this paper the performance characteristics of the medium access protocol---a slotted persistent CSMA/CD protocol---of a twisted pair home network are investigated. Using a dedicated semi-Markov model throughput results are obtained by analyzing an overload situation.

Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'93), vol. 25 of Simulation Series, pages 293-299, 1993. Full paper.

Workshop contributions

Multi-terminal decision diagrams: a data structure for numerical integration.
C. Baier, J-P. Katoen, H. Hermanns.
Proceedings 1th Workshop on Symbolic Model Checking (SMC'99), 1999. Full paper.

General purpose discrete-event simulation using SPADES.
P. R. D'Argenio, J-P. Katoen, E. Brinksma.
Proceedings 6th Workshop on Process Algebra and Performance Modelling (PAPM'98), pages 85-102, 1998. Full paper.

Pomsets for message sequence charts.
J-P. Katoen, L. Lambert.
Proceedings 8th German Workshop on Formal Description Techniques for Distributed Systems (FBT'98), pages 197-208, Shaker Verlag, 1998. Full paper.

A compositional approach to generalised semi-Markov processes.
P. R. D'Argenio, J-P. Katoen, E. Brinksma.
Proceedings 4th Workshop on Discrete-Event Systems (WODES'98), pages 391-397, IEE Press, 1998. Full paper.

Automatic verification of a lip-synchronisation algorithm using UPPAAL (extended abstract).
H. Bowman, G. Faconti, J-P. Katoen, D. Latella, M. Massink.
Proceedings 3rd Workshop on Formal Methods for Industrial Critical Systems (FMICS'98), pages 97-124, SMC Press, 1998. Full paper.

A stochastic automaton model and its algebraic approach.
P. R. D'Argenio, J-P. Katoen, E. Brinksma.
Proceedings 5th Workshop on Process Algebra and Performance Modelling (PAPM'97), CTIT Technical Report 97-09, pages 1-17, 1997. Full paper.

Stochastic simulation of event structures.
J-P. Katoen, E. Brinksma, D. Latella, R. Langerak.
Proceedings 4th Workshop on Process Algebra and Performance Modelling (PAPM'96), pages 21-40, CLUT Press, 1996. Full paper.

Modeling and verifying a bounded retransmission protocol.
P.R. D'Argenio, J-P. Katoen, T. Ruys, G.J. Tretmans.
Proceedings 1st Workshop on Applied Formal Methods in System Design, pages 114-128, University of Maribor Press, 1996. Full paper.

Reference configurations for UMTS.
W. van den Broek, J-P. Katoen.
Proceedings 2nd Workshop on Mobile Multimedia Communications, 1995. Full paper.

Performance analysis and true concurrency semantics.
E. Brinksma, J-P. Katoen, R. Langerak, D. Latella.
In T. Rus and C. Rattray (eds), Theories and experiences for real-time system development (ARTS'93), pages 309-337, World Scientific, 1994. Full paper.

Algebraic specification of dynamic leader election protocols in broadcast networks.
J.J. Brunekreef, J-P. Katoen, R.L.C. Koymans, S. Mauw.
Proceedings 2nd Workshop on Algebra of Communicating Processes (ACP'94), Workshops in Computing, pages 338-357,  Springer, 1994.  Full paper.

A UMTS network architecture.
J-P. Katoen, S. Abdelkrime, I. Baccaro.
Proceedings 2nd RACE Mobile Telecommunications Workshop, pages 285-290, 1994. Full paper.

A parallel program for recognizing P-invariant segments.
J-P. Katoen, B. Schoenmakers.
Proceedings 2nd Workshop on Algorithms and Parallel VLSI Architectures, North-Holland, pages 79-85, 1992. Full paper

The home system architecture definition: a survey.
J-P. Katoen, M.C. Vlot.
Proceedings European Conference on Integrated Home Applications, 1991.