Selected Papers of the Conference ''Tools and Algorithms for the Construction and Analysis of Systems 2007''

2007

Editors: Michael R A Huth, Orna Grumberg

We are pleased to introduce five papers that were published in a conference version in the proceedings of the Thirteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), held as part of the European Joint Conferences on Theory and Practice of Software (ETAPS) which ran from 24 March until 1 April 2007 in Braga, Portugal. These papers were then rewritten and extended as journal papers, by our invitation. The criteria for inviting papers were that the papers were amongst the top papers published in the TACAS 2007 proceedings, and that the papers reected well the intent of this journal: logical methods in computer science. So we very much hope that this special issue will be enjoyed by the readership of this journal.

The paper "Model Checking Probabilistic Timed Automata with One or Two Clocks" by Marcin Jurdzinski, Jeremy Sproston, and Francois Laroussinie derives novel complexity results for various model-checking problems for probabilistic timed automata with one or two clocks, improving markedly on the state-of-the-art in decision problems for probabilistic timed automata.

The paper "Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations" by Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, and David N. Jansen devises novel algorithms for deciding simulation relations for different kinds of probabilistic models and different notions of observability. These algorithms exploit parametric flow techniques to achieve better upper bounds for the complexity of these decision problems.

The paper "Multi-Objective Model Checking of Markov Decision Processes" by Kousha Etessami, Marta Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis provides efficient algorithms for deciding whether multiple objectives (given as omega-regular or LTL properties) can all be met with at least a specified objective-dependent probability. Also, approximate Pareto curves are shown to be efficiently computable for these models.

The paper "Antichains for the Automata-Based Approach to Model-Checking" by Laurent Doyen and Jean-Francois Raskin proposes and then evaluates algorithms that solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata by means of antichains.

The paper "A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes" by Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Yan Jurski, and Mihaela Sighireanu uses Colored Petri Nets to develop a framework in which one can reason about unbounded and dynamic networks of infinite-state processes. To that end, the authors develop a Coloring Markings Logic for describing configurations of colored Petri nets, and then show the decidability of satisfiability for a fragment of that logic.

Our special thanks go to the authors for their contributions, and to the anonymous referees for their timely and valuable reviews.

Orna Grumberg and Michael Huth
Guest Editors and PC Co-Chairs of TACAS 2007


1. Model Checking Probabilistic Timed Automata with One or Two Clocks

Jurdzinski, Marcin ; Laroussinie, Francois ; Sproston, Jeremy.
Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic timed automata which have one or two clocks. Firstly, we show that PCTL probabilistic model-checking problems (such […]

2. Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations

Zhang, Lijun ; Hermanns, Holger ; Eisenbrand, Friedrich ; Jansen, David N..
Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. However, decision algorithms for strong and weak simulation over Markov chains, and for strong simulation […]

3. Multi-Objective Model Checking of Markov Decision Processes

Etessami, Kousha ; Kwiatkowska, Marta ; Vardi, Moshe Y. ; Yannakakis, Mihalis.
We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (ømega -regular or LTL) properties \varphi\_i, and probabilities r\_i \epsilon [0,1], i=1,...,k, we ask whether there exists […]

4. Antichains for the Automata-Based Approach to Model-Checking

Doyen, Laurent ; Raskin, Jean-Francois.
We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be […]

5. A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes

Bouajjani, Ahmed ; Dragoi, Cezara ; Enea, Constantin ; Jurski, Yan ; Sighireanu, Mihaela.
We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over […]