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

Guest Editors and PC Co-Chairs of TACAS 2007

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 as determining whether a set of target states can be reached with probability at least 0.99 regardless of how nondeterminism is resolved) are PTIME-complete for one-clock probabilistic timed automata, and are EXPTIME-complete for probabilistic timed automata with two clocks. Secondly, we show that, for one-clock probabilistic timed automata, the model-checking problem for the probabilistic timed temporal logic PCTL is EXPTIME-complete. However, the model-checking problem for the subclass of PCTL which does not permit both punctual timing bounds, which require the occurrence of an event at an exact time point, and comparisons with probability bounds other than 0 or 1, is PTIME-complete for one-clock probabilistic timed automata.

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 over probabilistic automata are not efficient, which makes it as yet unclear whether they can be used as effectively as their non-probabilistic counterparts. This paper presents drastically improved algorithms to decide whether some (discrete- or continuous-time) Markov chain strongly or weakly simulates another, or whether a probabilistic automaton strongly simulates another. The key innovation is the use of parametric maximum flow techniques to amortize computations. We also present a novel algorithm for deciding strong probabilistic simulation preorders on probabilistic automata, which has polynomial complexity via a reduction to an LP problem. When extending the algorithms for probabilistic automata to their continuous-time counterpart, we retain the same complexity for both strong and strong probabilistic simulations.

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 (\omega -regular or LTL) properties \varphi\_i, and probabilities r\_i \epsilon [0,1], i=1,...,k, we ask whether there exists a strategy \sigma for the controller such that, for all i, the probability that a trajectory of M controlled by \sigma satisfies \varphi\_i is at least r\_i. We provide an algorithm that decides whether there exists such a strategy and if so produces it, and which runs in time polynomial in the size of the MDP. Such a strategy may require the use of both randomization and memory. We also consider more general multi-objective \omega -regular queries, which we motivate with an application to assume-guarantee compositional reasoning for probabilistic systems. Note that there can be trade-offs between different properties: satisfying property \varphi\_1 with high probability may necessitate satisfying \varphi\_2 with low probability. Viewing this as a multi-objective optimization problem, we want information about the "trade-off curve" or Pareto curve for maximizing the probabilities of different properties. We show that one can compute an approximate Pareto curve with respect to a set of \omega -regular properties in time polynomial in the size of the MDP. Our quantitative upper bounds use LP methods. We also study qualitative multi-objective model checking problems, and […]

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 exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of the algorithm to check the universality of Buechi automata using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude.

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 some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens. We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.