IFIP WG 2.2 Meeting Warsaw

September 20-22, 2010

Titles and abstracts of talks

(in chronological order)

Speaker: Stefan Merz
Title: Reduction Revisited: Verifying Round-Based Distributed Algorithms

Abstract:

Distributed algorithms are often quite subtle, in the way they operate and in the assumptions they make. Formal verification is therefore crucial in distributed computing. To facilitate their design and understanding, many existing distributed algorithms are structured in rounds: each process first sends messages, then receives messages from other processes, and finally makes a local state transition. However, existing formal models of distributed algorithms do not take advantage of this structure, but are based on a fine-grained description of systems whose individual processes are represented by communicating state machines.

Reduction theorems for concurrent and distributed algorithm have been studied since Lipton's seminal paper in 1975. Broadly speaking, they aim at pretending that certain sequences of events happen indivisibly, thus allowing verification to be carried out over coarser-grained models of algorithms and systems. We revisit this line of research and contribute a reduction theorem for distributed algorithms that are organized in communication-closed rounds, demonstrating its benefits on the verification of several consensus algorithms using model checking and theorem proving.

(Joint work with Bernadette Charron-Bost)

Speaker: Marjan Sirjani
Title: The Coordination Language Reo, its Formal Semantics and Analysis Techniques

Abstract:

In this talk I’ll explain the coordination language, Reo. Then, I’ll give an overview of its formal semantics, Constraint Automata. Some analysis techniques for Reo and Constraint Automata will be presented.

(Tutorial talk)

Speaker: Naoki Kobayashi
Title: Model-Checking Higher-Order Programs

Abstract:

The talk gives an overview of a series of our recent work on higher-order model checking and its applications to program verification. We first introducehigher-order model checking (more precisely, model checking of higher order recursion schemes) and show how verification problems for higher-order functional programs can be reduced to the higher-order model checking. We then show how the higher-order model checking can be reduced to a type checking problem. Based on the reduction, we have developed a realistic algorithm for higher-order model checking and implemented a higher-order model checker TRecS, which works reasonably well despite the extremely high worst case complexity. We conclude the talk by discussing advantages of higher-order model checking, and ongoing and future work to construct software model checkers for higher-order functional programs on top of the higher order model checker.

Speaker: Matthew Hennessy
Title: A Theory of Nondeterministic and Probabilistic Processes

Abstract:

We give an overview of a semantic theory of processes which exhibit both nondeterministic and probabilistic behaviour. Our approach is based on the ability of processes to pass tests, representing the possible interactions between processes and their observers. We explain how such behaviour, expressed in terms of preorder between processes, can be captured by a coinductively defined notion of probabilistic simulation.

References:

(1) Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan.
Characterising Testing Preorders for Finite Probabilistic Processes, LMCS (Logical Methods
in Computer Science), 2008

(2) Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan.
Testing Finitary Probabilistic Processes, CONCUR 2009

Speaker: Christel Baier
Title: Quantitative Analysis of Randomized Systems and Probabilistic Automata

Abstract:

The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an omega-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the “worst-case” is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account. As in the nonprobabilistic case, the commutativity of independent concurrent actions can be used to avoid redundancies in the system model and to increase the efficiency of the quantitative analysis. However, there are certain phenomena that are specific for the probabilistic case and require additional conditions for the reduced model to ensure that the worst-case probabilities are preserved. Related to this observation is also the fact that the worst-case analysis that ranges over all schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partialinformation schedulers yield more realistic worst-case probabilities, but computationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers.

(Joint work with Nathalie Bertrand, Frank Ciesinski, and Marcus Groesser)

Speaker: Antonin Kucera
Title: Properties of Stochastic Games with Branching-Time Winning Objectives

Abstract:

Stochastic games are directed binary graphs where each vertex belongs either to Player-I, Player-II, and it is stochastic. The talk surveys recent results about stochastic games with branching-time winning objectives that are specified as formulae of probabilistic branching-time logics such as PCTL or PCTL*. The goal of Player-I is to satisfy a given formula, while Player-II aims at the opposite. Such games are generally not determined, and winning strategies (if they exist) may require both memory and randomization. Still, the winner in such games can be determined effectively in some cases.

(Joint work with Stefan Kiefer and Michael Luttenberger)

References:

T. Brázdil, V. Forejt, and A. Kucera.
Controller Synthesis and Verification for Markov Decision Processes with
Qualitative Branching Time Objectives.
In Proceedings of 35th International Colloquium on Automata, Languages and
Programming (ICALP 2008), pages 148-159, volume 5126 of LNCS. Springer, 2008.

T. Brázdil, V. Brožek, V. Forejt, and A. Kucera.
Stochastic Games with Branching-Time Winning Objectives.
In Proceedings of 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006),
pages 349-358, IEEE Computer Society, 2006.

Speaker: Joost-Pieter Katoen
Title: Concurrency, Interaction, Abstraction and Randomness

Abstract:

We consider a continuous-time stochastic model —called interactive Markov chains (IMCs)— which allows interaction and concurrency in a process-algebraic fashion. We discuss notions of strong and weak (bi)simulation and their congruence properties. We show how simulation pre-congruences provide the basis for compositional abstraction where abstract models are a mixture of interval IMCs and modal transition systems.

A key problem in model checking IMCs, in fact stochastic real-time games, is computing maximal time-bounded reachability probabilities. We show a discretisation approach to determine optimal timed (measurable) policies, and report on some practical results.

Finally, we show that IMCs are the semantical backbone for higher-level formalisms from various domains such as generalized stochastic Petri nets (GSPNs) used in performance evaluation, dynamic fault trees (DFTs) used in reliability and safety engineering, and AADL, a standardised language in hardware/software co-design.

Speaker: Jan Rutten
Title: Stream differential equations: theory and applications

Abstract:

Coinduction has come to play an ever more important role in theoretical computer science, for the specification of and reasoning about infinite data structures and, more generally, automata with infinite behaviour.

In this talk, we shall focus on a recently introduced formalism for coinductive definitions: behavioural differential equations, with which one specifies behaviour in terms of initial outputs and behavioural derivatives (next state operators). Our emphasis will be on the elementary calculus of streams (infinite sequences), of which we shall
discuss the basic theory, developed in close analogy to mathematical analysis.

As an application area, we will mention a calculus for periodic stream operators. Using this, we will give a new and transparent proof of Moessner's theorem using coinduction. This theorem (from 1951 - 1952) gives a suprising construction for the stream of powers n^k of the natural numbers (such as 1,8,27,64, ... for k=3) out of the stream of natural numbers by an alternating process of stream sampling and taking partial sums.

Speaker: Peter D. Mosses
Title: On bisimulation and modularity

Abstract:

Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language.

In this talk we consider preservation of sound equations for several notions of bisimilarity on open terms: closed-instance (ci-) bisimilarity and formal-hypothesis (fh-) bisimilarity, both due to De Simone [1] and hypothesis-preserving (hp-) bisimilarity, due to Rensink [2].

We give simple examples showing that for ci-bisimilarity, sound equations on open terms are not preserved by disjoint extensions. For both fh-bisimilarity and hp-bisimilarity, arbitrary sound equations on open terms are preserved by all disjoint extensions which do not add labels. Moreover, for slight variations of fh- and hp-bisimilarity, all sound equations are preserved by arbitrary disjoint extensions. See [3] for further details and proofs.

References:

[1] R. de Simone (1985): Higher-Level Synchronizing Devices
in MEIJE-SCCS. Theoretical Computer Science 37, pp. 245â€“267.

[2] A. Rensink (2000): Bisimilarity of Open Terms.
Information and Computation 156, pp. 345â€“385.

[3] P. D. Mosses, M. R. Mousavi & M. A. Reniers (2010):
Robustness of Equations Under Operational Extensions.
Proc. EXPRESS 2010. EPTCS, to appear; preliminary version available

Speaker: Philippe Darondeau
Title: Some Questions about Security and Concurrency

Abstract:

In [1], we have shown that Larsen's modal automata enriched with final states are a convenient framework for specifying services and for computing the optimal control that enforces such specifications on a given service provider. We ask whether similar control may be computed for more powerful specification frameworks, e.g., based on session types. In [2], we have defined an algorithm for computing the optimal control that enforces the opacity of a given predicate on the runs of a system (representing some secret). Based on this work, we propose to study opacity games where each player tries to maintain the opacity of some secrets and to break the opacity of other secrets. In [3], we have established the decidability of non-interference and intransitive non-interference for unbounded Petri nets. We ask whether one could find well behaved security properties between non-interference and opacity.

References:

[1] R. de Simone (1985): Higher-Level Synchronizing Devices
in MEIJE-SCCS. Theoretical Computer Science 37, pp. 245â€“267.

[1] Supervisory Control for Modal Specifications of Services.
P. Darondeau, J. Dubreil, H. Marchand. Wodes, IEEE (2010) 428-435

[2] Supervisory Control of Opacity.
J. Dubreil, P. Darondeau, H. Marchand. IEEE-TAC 55(5) (2010) 1089-1100

[3] On the Decidability of Non Interference over Unbounded Petri Nets.
E. Best, P. Darondeau, R. Gorrieri. 8th International Workshop on Security Issues in Concurrency (SecCo 2010).

Speaker: Maciej Koutny
Title: Step Coverability Algorithms for Concurrent Systems

Abstract:

Coverability (of states) is an important, useful notion for the behavioural analysis of distributed dynamic systems. For systems like Petri nets, the classical Karp-Miller coverability tree construction is the basis for algorithms to decide questions related to the capacity of local states. We consider a modification of this construction which would allow one to deal with dynamic behaviour consisting of concurrent steps rather than single occurrences of transitions. This leads to an action-based extension of the notion of coverability, viewing bandwidth as a resource. However, when certain constraints are imposed on the steps, systems may exhibit non-monotonic behaviour. In those cases, new criteria for the termination of the step coverability tree construction are needed. We investigate a general class of Petri nets modelling systems that consist of components communicating through shared buffers and that operate under a maximally concurrent step semantics. Based on the description of their behaviour, we derive a correctly terminating step coverability tree construction for these Petri nets.

Speaker: K.V.S Prasad
Title: A pointer to Computational Modeling in Biology

Abstract:

Proteins typically have many sites at which they may bind to other molecules, and so can exist in many states. Mathematical models of biochemical systems can tackle this combinatorial explosion by simplifying assumptions, but these are hard to make, and obscure or remove essential properties of the system. New languages such as SPiM (http://research.microsoft.com/en-us/projects/spim/), Kappa (http://base.org/) and BioNetGen (http://bionetgen.org/index.php/Main_Page) allow concise yet unambiguous and detailed descriptions of systems, which can then also be simulated stochastically.

These languages were derived from systems like the stochastic pi-calculus, and allow agent- or rule-based descriptions of systems. Several chemical reactions can be replaced by a single rule that partially specifies the reactants: eg., giving the states of only those binding sites relevant to the class of reaction. Focusing on local aspects helps too: a system of m metals and h halogens, say, needs not m*h reactions, but just m+h reactions saying for each element how it forms ions.

Speaker: Andrzej Tarlecki
Title: Some nuances of many-sorted algebra

Abstract:

It has been a common belief that the standard results of universal algebra as developed since the work of Birkhoff and others in the thirties carry over without much change to the framework of many-sorted algebras. Perhaps the only notable exception widely noticed by the community is the care needed in the treatment of many-sorted equational logic. However, while the standard results remain valid in essence in the many-sorted frameworks, some nuances and technicalities require considerably more care in formulation and proof of the results. I give some examples of such situation, indicating how equational calculus, Birkhoff's variety theorem and interpolation results should be adjusted.

Speaker: Willem Paul de Roever
Title: What is in a Step: New Perspectives on a Classical Question

Abstract:

In their seminal 1991 paper "What is in a Step: On the Semantics of Statecharts", Pnueli and Shalev showed how, in the presence of global consistency and while observing causality, the synchronous language Statecharts can be given coinciding operational and declarative step semantics. Over the past decade, this semantics has been supplemented with order-theoretic, denotational and fully abstract, axiomatic and game-theoretic characterizations, thus revealing itself as a rather canonical interpretation of the synchrony hypothesis. These characterizations are surveyed and used to emphasize the close but not widely known relations of Statecharts to the synchronous language Esterel and to the field of logic programming. Additionally, we highlight some early reminiscences on Amir Pnueli's contributions to characterize the semantics of Statecharts.

(Joint work with Gerald Lüttgen, and Michael Mendler)

Speaker: Markus Müller-Olm
Title: Lock-join-sensitive Analysis of Recursive Programs with Thread-creation

Abstract:

We give a summary of our work on automata-based optimal analysis of programs with thread-creation and potentially recursive procedures. Specifically, we introduce dynamic pushdown networks (DPNs) that extend pushdown processes by thread creation as a model for such programs, introduce their semantics, and summarize basic results on
reachability analysis and its applications. Then, we move from a word-shaped to tree-shaped views of executions which allows us to impose regular constraints on the communicated actions in symbolic backward analysis or even to describe the entire set of executions by regular means. This in turn enables us to do lock-join-sensitive reachability analysis as the set of action trees that posess a lock-join-sensitive schedule turns out to be regular.

The talk is based on papers presented at CONCUR 2005 and CAV 2009 and ongoing recent work. It reports on joint work with various people.

Speaker: Ernst-Rüdiger Olderog
Title: Layered Composition for Data-Enriched Real-Time Systems

Abstract:

We investigate techniques that aim at easier verification of data-enriched real-time systems, modelled as networks of extended timed automata (ETA) running in parallel. To this end, we reconsider the work of Zwiers and Janssen developed in the early 1990s on layered composition in the setting of ETA. First introduce a syntactic notion of independence and an operator for layered composition of ETA. Under certain independence conditions, the Communication Closed Layer (CCL) laws are shown to hold for ETA. Next, we introduce input/output (i/o) and partial-order (po) equivalences, and show that they are preserved when the layered composition operator is replaced by sequential composition within the CCL laws. Finally, we demonstrate the effect of layered composition by revisiting a case study of the UPPAAL model checker for ETA, a collision avoidance protocol developed for an audio/video system of Bang and Olufsen.

(joint work with Mani Swaminathan)