Preface

This volume contains the proceedings of the 15th International Workshop on Verification of Infinite-State Systems (INFINITY'13). The workshop was held in Hanoi, Vietnam on October 14, 2013, as a satellite event to the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13).

The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.

• Infinite-state models of software/hardware systems
• Abstraction techniques for infinite-state systems
• Symbolic analysis techniques and data structures for representing infinite state spaces
• Model-checking, static analysis, abstract interpretation, preorder/equivalence-checking, and control synthesis for infinite-state systems
• Parameterized networks of parallel processes, dynamic networks, mobile systems
• Systems with unbounded dynamic data and control structures
  (recursion, dynamic instantiation of processes, dynamic linked data structures, unbounded communication channels, web services, infinite data domains)
• Probabilistic and timed systems
• Games in modeling and verification of infinite-state systems
• Verification techniques for security properties, cryptographic protocols
• Verification techniques for systems biology

This volume contains seven contributions: three regular papers, one presentation, and three invited tutorials. Each regular paper was reviewed by four different reviewers. The papers were refereed by the program committee and by external referee Cong Quy Trinh, whose help is gratefully acknowledged. Each invited tutorial was reviewed by the editors before acceptance. Moreover, the program committee of INFINITY 2013 has selected the following presentation:

• Barbara König and Jan Stückrath, Decidability Results for Well-structured Graph Transformation Systems

The program of INFINITY 2013 was further enriched by four invited talks given by

• Laurent Doyen, LSV, ENS Cachan & CNRS, France.
• Oded Maler, CNRS-VERIMAG, University of Grenoble, France.
• Doron Peled, Bar Ilan University, Israel.
• Dominik Wojtczak, University of Liverpool, UK.

The INFINITY'13 workshop was attended by 21 participants. It has been organized as a satellite event to ATVA'13. We thank the authors for their contributions, the programme committee members for reviewing and selecting the papers and the invited talks, and the ATVA organizing committee Mizuhito Ogawa and Truong Anh Hoang for their support.

The final proceedings will appear in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. We thank Rob Van Glabbeek (Editor-in-Chief) and the board of the EPTCS for making this possible.

Bordeaux and Brno, December 2013

Lorenzo Clemente and Lukáš Holík

Organizers and Program Chairs

Program Committee

Automated Analysis of Probabilistic Infinite-state Systems

In this talk we survey the state of the art in the automated analysis of several classes of finitely-presentable infinite-state probabilistic models which combine probabilistic, recursive and in many cases also controlled or more general game behaviour. Unreliability is inherent to almost all physical systems, e.g. telecommunication networks, distributed systems, railway connections. Software systems, designed with robustness and efficiency in mind, often make explicit use of randomness, thus exhibiting probabilistic behaviour. Also, even if a system or a program behaves deterministically, the environment were it operates is in many cases either unknown or very complex. In such situations the best we can hope for is to statistically quantify the behaviour of the environment and analyse the performance of our model in such a probabilistic setting. It is common to model purely probabilistic systems as finite-state Markov Chains or as Markov Decision Processes if the system is both probabilistic and controlled. However, to faithfully represent the behaviour of many naturally occurring systems one really needs to represent them as infinite-state Markov Chains or Markov Decision Processes. This is because finite-state probabilistic models differ significantly from infinite-state ones, e.g. in finite-state systems no null recurrent states can occur, i.e. states that are revisited with probability 1, but with infinite expected time before this happens.

The finitely-presentable infinite-state probabilistic models studied in the literature include Multi-Type Branching Processes (see, e.g. [12, 10]), Stochastic Context-Free Grammars (see, e.g. [13, 1]), Quasi-Death-Birth processes (see, e.g. [14, 15]), "random walks with back-buttons" [9], Recursive Markov Chains [8] and probabilistic Pushdown Systems [4]. These models found applications in domains as diverse as population dynamics, nuclear chain reactions, natural language processing, biological sequence analysis, red blood cells formation, queueing theory, modelling web surfing and finally model checking of probabilistic procedural programs. The relationship of the expressive power of these particular models have been extensively studied, e.g. in [7] where a tight connection was established to the the models used in the queueing theory, but the first natural model that subsumes all of the mentioned models was defined in [11].

The fundamental quantitative analysis of these models can be done by constructing a specific system of monotone polynomial equations and finding its least nonnegative fixed point. In order to find this fixed point efficiently we can use, e.g. numerical approximation methods such as Jacobi iteration, Gauss-Seidel iteration or a decomposed variant of the Newton's method as described in [8]. A detailed analysis of the theoretical performance of the Newton's method when applied in this setting was done in [3, 5]. Here we look instead on how well it performs in practice and describe a tool called PReMo [17] (Probabilistic Recursive Models analyser) which implements highly optimised versions of these approximation algorithms in Java. Using simple tailored-made input languages PReMo is able to accept Recursive Markov Chains and Stochastic Context-Free grammars as an input, while the other models can be easily translated into these ones. PReMo is able to perform all kind of analyses such as computing the termination probability (as described in [8]), the expected termination time (as in [6]) or the standard deviation of that time (as in [2]) among others. PReMo's performance was tested on Stochastic Context-Free Grammars derived from the Penn Treebank corpora in [17], on queuing models in [7] and on many other examples in [16].

The general domain of finitely-presented infinite-state probabilistic models is a rich and fascinating field of study that is getting more and more attention. Many important questions regarding the computational complexity of their analysis were already addressed and there is a tool that is able to analyse them efficiently. However, many theoretical questions still remain open, and there is still a potential of improving the performance of PReMo, the range of quantitative analyses and input models it supports.

References

1. Richard Durbin (1998): Biological sequence analysis: probabilistic models of proteins and nucleic acids, doi:10.1017/CBO9780511790492. Cambridge university press.
2. J. Esparza, A. Kucera & R. Mayr (2005): Quantitative analysis of probabilistic pushdown automata: expectations and variances. In: 20th Annual IEEE Symposium on Logic in Computer Science, 2005. LICS 2005. Proceedings, pp. 117–126, doi:10.1109/LICS.2005.39.
3. Javier Esparza, Stefan Kiefer & Michael Luttenberger (2010): Computing the Least Fixed Point of Positive Polynomial Systems. SIAM Journal on Computing 39(6), pp. 2282–2335, doi:10.1137/090749591.
4. Javier Esparza, Antonin Kucera & Richard Mayr (2004): Model Checking Probabilistic Pushdown Automata. In: Proceedings of the 19th Symposium on Logic in Computer Science, LICS '04. IEEE Computer Society, Washington, DC, USA, pp. 12–21, doi:10.1109/LICS.2004.23.
5. Kousha Etessami, Alistair Stewart & Mihalis Yannakakis (2012): Polynomial Time Algorithms for Multi-type Branching Processes and Stochastic Context-free Grammars. In: Proceedings of the 44th Symposium on Theory of Computing, STOC '12. ACM, New York, NY, USA, pp. 579–588, doi:10.1145/2213977.2214030.
6. Kousha Etessami, Dominik Wojtczak & Mihalis Yannakakis (2008): Recursive Stochastic Games with Positive Rewards. In: Proceedings of the 35th International Colloquium on Automata, Languages and Programming, Part I, ICALP '08. Springer-Verlag, Berlin, Heidelberg, pp. 711–723, doi:10.1007/978-3-540-70575-8_58.
7. Kousha Etessami, Dominik Wojtczak & Mihalis Yannakakis (2010): Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems. Perform. Eval. 67(9), pp. 837–857, doi:10.1016/j.peva.2009.12.009.
8. Kousha Etessami & Mihalis Yannakakis (2009): Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations. J. ACM 56(1), pp. 1–66, doi:10.1145/1462153.1462154.
9. Ronald Fagin, Anna R. Karlin, Jon Kleinberg, Prabhakar Raghavan, Sridhar Rajagopalan, Ronitt Rubinfeld, Madhu Sudan & Andrew Tomkins (2000): Random Walks with "Back Buttons". In: Proceedings of the 32nd Symposium on Theory of Computing, STOC '00. ACM, New York, NY, USA, pp. 484–493, doi:10.1145/335305.335362.
10. Theodore E. Harris (2002): The theory of branching processes. Courier Dover Publications.
11. Stefan Kiefer & Dominik Wojtczak (2011): On Probabilistic Parallel Programs with Process Creation and Synchronisation. In: Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'11. Springer-Verlag, Berlin, Heidelberg, pp. 296–310, doi:10.1007/978-3-642-19835-9_28.
12. Andrei Nikolaevitch Kolmogorov & B. A. Sevastyanov (1947): The calculation of final probabilities for branching random processes. Doklady 56, pp. 783–786, doi:10.1007/978-94-011-2260-3_33.
13. Christopher D. Manning & Hinrich Schütze (1999): Foundations of Statistical Natural Language Processing. MIT Press, Cambridge, MA, USA, doi:10.1145/601858.601867.
14. Marcel F. Neuts (1981): Matrix-geometric solutions in stochastic models: an algorithmic approach. Courier Dover Publications.
15. Marcel F. Neuts (1989): Structured stochastic matrices of M/G/1 type and their applications 5. CRC Press.
16. Dominik Wojtczak (2009): Recursive probabilistic models: efficient analysis and implementation. Ph.D. thesis. University of Edinburgh.
17. Dominik Wojtczak & Kousha Etessami (2007): PReMo: An Analyzer for Probabilistic Recursive Models. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'07. Springer-Verlag, Berlin, Heidelberg, pp. 66–71, doi:10.1007/978-3-540-71209-1_7.

Decidability Results for Well-structured Graph Transformation Systems

Well-structured transition systems [1, 4] are one of the main sources for decidability results for infinite-state systems. Well-structured transition systems equip a state space with a partial order, which must be a well-quasi-order and a simulation relation for the transition relation. If a system can be seen as a well-structured transition system, one can decide the coverability problem, i.e., the problem of verifying whether, from a given start state, one can reach a state that covers a final state, i.e., is larger than the final state with respect to the chosen order by a generic backward reachability algorithm. Often, these given final states, and all larger states, are considered to be error states and one can hence check whether an error state is reachable.

This can also be done for graph transformation systems [9], a natural specification language for concurrent, distributed systems with a variable topology. In those systems states are represented by (hyper-)graphs and state changes by (local) transformation rules, consisting of a left-hand and a right-hand side.

In [5] we showed how certain lossy graph transformation systems with edge contraction rules can be viewed as well-structured transition systems with respect to the graph minor ordering [7, 8] and applied the theory to verify a leader election protocol. In later work [2] we treated another case study and analysed a termination detection protocol. The technique works for arbitrary graphs, since the minor ordering is a well-quasi-order on all graphs, but requires certain restrictions on the rule sets to obtain well-structuredness, namely the existence of edge contraction rules.

Here we will extend the approach of [5] to a general framework [6], which can handle arbitrary orders and state sufficient conditions for the backward search to be correct. We consider the subgraph ordering and the induced subgraph ordering as alternatives to the minor ordering.

Opposed to the minor ordering, the subgraph ordering is not a well-quasi-order on the set of all graphs, but only on those graphs where the length of paths is bounded. This results in a trade-off: while the stricter order allows us to consider all possible sets of graph transformation rules (we show that these systems are all well-structured w.r.t. the subgraph ordering), we have to make sure to consider a system where only graphs satisfying this restriction are reachable. Furthermore, we gain precision in the specification of final graphs, since we can represent them via subgraphs instead of minors. The induced subgraph ordering, apart from being more precise in the specification of error graphs, in addition allows restricted negative application conditions on the rules. It turns out that the results and proofs of [5] can be transferred to this new setting.

Apart from the orders mentioned above, there are various other well-quasi-orders on graphs that could be used [3], leading to different classes of systems and different notions of coverability. Our framework can handle such partial orders if they can be represented by (partial) graph morphisms and satisfy some preservation criteria with respect to pushouts of graphs.

References

1. Parosh Aziz Abdulla, Kārlis Cerāns, Bengt Jonsson & Yih-Kuen Tsay (1996): General Decidability Theorems for Infinite-State Systems. In: Proc. of LICS '96. IEEE, pp. 313–321, doi:10.1109/LICS.1996.561359.
2. Nathalie Bertrand, Giorgio Delzanno, Barbara König, Arnaud Sangnier & Jan Stückrath (2012): On the Decidability Status of Reachability and Coverability in Graph Transformation Systems. In: Proc. of RTA '12, LIPIcs 15. Schloss Dagstuhl – Leibniz Center for Informatics, pp. 101–116, doi:10.4230/LIPIcs.RTA.2012.101.
3. Michael R. Fellows, Danny Hermelin & Frances A. Rosamond (2009): Well-Quasi-Orders in Subclasses of Bounded Treewidth Graphs. In: Proc. of IWPEC '09 (Parameterized and Exact Computation). Springer, pp. 149–160, doi:10.1007/978-3-642-11269-0_12. LNCS 5917.
4. Alain Finkel & Philippe Schnoebelen (2001): Well-Structured Transition Systems Everywhere! Theoretical Computer Science 256(1-2), pp. 63–92, doi:10.1016/S0304-3975(00)00102-X.
5. Salil Joshi & Barbara König (2008): Applying the Graph Minor Theorem to the Verification of Graph Transformation Systems. In: Proc. of CAV '08. Springer, pp. 214–226, doi:10.1007/978-3-540-70545-1_21. LNCS 5123.
6. Barbara König & Jan Stückrath (2013): A General Framework for Well-Structured Graph Transformation Systems. Submitted for publication.
7. Neil Robertson & Paul Seymour (2004): Graph minors. XX. Wagner's conjecture. Journal of Combinatorial Theory, Series B 92(2), pp. 325–357, doi:10.1016/j.jctb.2004.08.001.
8. Neil Robertson & Paul Seymour (2010): Graph minors XXIII. Nash-Williams' immersion conjecture. Journal of Combinatorial Theory Series B 100, pp. 181–205, doi:10.1016/j.jctb.2009.07.003.
9. Grzegorz Rozenberg (1997): Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations. World Scientific.