25 - 29 September 2000, Oldenburg, Germany.

Controlling Interference in Ambients

The talk is based on joint work with Francesca Levi (University of Pisa), published in the proceedings of POPL'00.

Efficient methods for model checking of Timed Petri Nets

- Introduction to model checking - automata-theoretic approach,
- Reduction methods for untimed global state approaches: on-the-fly, po-reductions, symbolic (BDDs), translation to SAT,
- Timed and untimed temporal logics: LTL, CTLS, ACTLS, LTL$_\Delta$, MITL, and TCTL,
- Translations from temporal logics to automata,
- Timed Petri Nets,
- Abstractions preserving timed and untimed temporal logics,
- Partial order reductions for Time Petr Nets.

- improving the variant of the geometric region method for defining abstract state spaces preserving properties of \CTLS\/ and \ACTLS\/ such that the structure of a verified formula is exploited,
- showing how to extend the po-reduction methods to deal with branching properties of Time Petri Nets.

- W. Penczek: Partial order reductions for checking branching properties of Timed Petri Nets, Proc. of CS\&P, Berlin, to appear, 2000.
- W. Penczek, M. Szreter, R. Gerth and R. Kuiper: Improving Partial Order Reductions for Universal Branching Timed Properties, Fundamenta Informaticae, to appear, 2000.
- M. Szreter and W. Penczek: More than one, less than all: Linear to Branching revisited, Proc. of CS\&P, Berlin, to appear, 2000.
- R. Gerth, R. Kuiper, D. Peled, and W. Penczek: A Partial Order Approach to Branching Time Logic Model Checking, Information and Computation, Vol. 150, No. 2, pp. 132-152, 1999.

Deciding low levels of the mu-calculus alternation hierarchy

I will show that it is EXPTIME-complete to decide if the language can be written using the least fixpoints only. The same bound also holds for terms with only the greatest fixpoints. The case of mixed (but not alternating) fixpoints is already much more difficult to solve. The subject is also a good occasion to give a very short summary of what is known about the alternation hierarchy.

Sticks and Stones: Making the Most of a Single Unbounded Dimension

Verifying Soft Deadlines with probabilistic Timed Automata

Using space-time duality to structure interaction systems

The aim of the talk is to present the space-time duality mechanism and to look at a few aspects of the interaction systems which have to be reconsidered in the view of space-time duality. Also, a few technical ingredients, most of them based on the network algebra approach, will be presented.

For more on this, one may have a look on the book: G. Stefanescu, Network Algebra, Springer-Verlag, London/Berlin/... http://funinf.cs.unibuc.ro/~ghstef/na/myAdv.html

On preservation of relative correctness

It is quite known that total program correctness is more difficult to prove than partial correctness. But it is most interesting to see that for preservation of total resp. partial correctness the situation is the other way round. This phenomenon has been first observed when compiling while-programs into flat assembly code with unconditional and conditional jumps [MOl95] and later when translating ALGOL-like programs with nested blocks, parameterless procedures and static scoping into flat assembly code augmented by subroutine and return jumps [MOW00,Wol00]. Source languages are assumed to be furnished with denotational (predicate transformer) semantics, target languages with operational step semantics.

The decisive difference is evoked by the premis whether divergence (infinite computation) is considered to be an unacceptable error (generalized total correctness) or to be an acceptable one (generalized partial correctness). The inductive proof of generalized total correctness preservation utilizers just a series of algebraic laws for assembly instructions semantics. But above that, proof of preservation of generalized partial correctness has to exploit a fixpoint characterization of the operational target semantics. In case divergence is unacceptable operational target semantics is indeed the least fixpoint of a certain functional, otherwise the largest fixpoint [MOl97,MOW99,MOW00,Wol00].

Easiness of proof might be an indication why software engineering in the past has favoured preservation of total correctness for software implementation. But in usual information processing outside process programming preservation of (generalized) partial correctness is at least as important, especially because realistic target machines with their finite resources cannot fulfill all total program correctness wishes.

Most realistic compilers do a lot of code optimizations like dead or redundant code elimination, code motion or unswitching. But often language and compiler manuals do not inform the users decently enough about correctness of optimizations, namely what conditions source programs must fulfill and what consequences on computing results are to be expected. Relative program correctness and its preservartion allow very precise investigations and delineations of these conditions and consequences [MOW99,MOW00,Wol00].

- [MOl95]
- M. Mueller-Olm. An Exercise in Compiler Verification. Kiel, 1995. Available from the author.
- [MOl97]
- M. Mueller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction. LNCS, Vol. 1283, Springer-Verlag, 1997.
- [MOW99]
- M. Mueller-Olm and A. Wolf. On Excusable and Inexcusable Failures: On an Adequate Notion of Translation Correctness. In J. Wing, J. Woodcock and J. Davies (eds.), FM '99 - Formal Methods. LNCS, vol. 1709, 1107 - 1127, Springer-Verlag, 1999.
- [MOW00]
- M. Mueller-Olm and A. Wolf. On the Translation of Procedures to Finite Machines: Abstraction allows a Clean Proof. In G. Smolka (ed.) Programming Languages and Systems. Proc. ESOP 2000, LNCS, vol. 1782, 290 - 304, Springer-Verlag, 2000.
- [Wol00]
- A. Wolf. Weakest Relative Precondition Semantics: Balancing Approved Theory and Realistic Translation Verification. Univ. Kiel, dissertation, subm. 2000.

Compositional Model Checking

Fault tolerant design in OUN specification language

Probabilistic asynchronous $\pi$-calculus

Realizing HMSC's by Distributable PN's

$\alpha$: A purely functional language with imperative language inside

The main characteristic of $\alpha$ is that it has environments as first-class objects. By using first-class environments, we can encapsulate imperative programs by treating imperative programs as environment tranformers. In this way, side-effects caused by the execution of imperative programs becomes invisible from outside.

We also discuss another usages of first-class environments. For example,
we show that given an abstract obtained by abstracting several variables,
we can instantiate any of these variables by specifying the name of
the variable to be instantiated and the value which will replace
the variable.