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.