LICS on Saturday, August 12th

FLoC Opening and Plenary Session (08:45‑10:00)
Chair: Moshe Vardi, Thomas Ball, Wolfram Schulte, Rajeev Alur

08:45‑09:00

Introduction and Welcome

09:00‑10:00

Randal E. Bryant (Carnegie Mellon University) Formal Verification of Infinite State Systems using Boolean Methods [ppt] Most successful automated formal verification tools are based on a bit-level model of computation. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers and similar tools can analyze all possible behaviors of very large, finite-state systems. For many hardware and software systems, we would like to go beyond bit-level models to handle systems that are truly infinite state, or that are better modeled as infinite-state systems. Examples include programs manipulating integer data, concurrency protocols involving arbitrary numbers of processes, and systems containing buffers where the sizes are described parametrically. Historically, much of the effort in verifying such systems involved automated theorem provers, requiring considerable guidance and expertise on the part of the user. We would like to devise approaches for these more powerful computational models that retain the desirable features of model checking, such as the high degree of automation and the ability to generate counterexamples. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is quite expressive, yet it still permits a decision procedure that transforms the formula into propositional logic and then uses a SAT solver. UCLID supports multiple forms of verification, requiring different levels of sophistication in the handling of quantifiers. We demonstrate UCLID's modeling and verification capabilities with such examples as out-of-order microprocessors and directory-based cache coherency protocols.

Break (10:00‑10:30)

Session 1: Complexity and Decidability (10:30‑12:30)
Chair: Stephan Kreutzer

10:30‑11:00	Mikolaj Bojanczyk (Warsaw University) Anca Muscholl (University of Paris 7) Thomas Schwentick (Universität Dortmund) Luc Segoufin (INRIA) Claire David Two-Variable Logic on Words with Data In a data word each position carries a label from a finite alphabet and a data value from some infinite domain. These models have been already considered in the realm of semistructured data, timed automata and extended temporal logics. We show that satisfiability for the two-variable first-order logic FO2(~,<,+1) is decidable over finite and over infinite data words, where ~ is a binary predicate testing the data value equality and +1,< are the usual successor and order predicates. The complexity of the problem is at least as hard as Petri net reachability. Several extensions of the logic are considered, some remain decidable while some are undecidable.
11:00‑11:30	Stephane Demri (LSV, ENS de Cachan) Ranko Lazic (University of Warwick) LTL with the Freeze Quantifier and Register Automata Temporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A data word is a word over a finite alphabet, together with a datum (an element of an infinite domain) at each position. Examples include timed words and XML documents. To refer to the data, temporal logics are extended with the freeze quantifier, first-order logics with predicates over the data domain, and automata with registers or pebbles. We investigate relative expressiveness and complexity of standard decision problems for LTL with the freeze quantifier, 2-variable first-order logic (FO^2) over data words, and register automata. The only predicate available on data is equality. Previously undiscovered connections among those formalisms, and to counter automata with incrementing errors, enable us to answer several questions left open in recent literature. We show that the future-time fragment of LTL with freeze which corresponds to FO^2 over finite data words can be extended considerably while preserving decidability, but at the expense of non-primitive recursive complexity, and that most of further extensions are undecidable. We also prove that surprisingly, over infinite data words, LTL with freeze and without the `until' operator, as well as nonemptiness of one-way universal register automata, are undecidable even when there is only 1 register.
11:30‑12:00	Guoqiang Pan (Rice University) Moshe Y. Vardi (Rice University and Microsoft Research) Fixed-Parameter Hierarchies inside PSPACE Treewidth measures the "tree-likeness" of structures. Many NP-complete problems, e.g., propositional satisfiability, are tractable on bounded-treewidth structures. In this work, we study the impact of treewidth bounds on QBF, a canonical PSPACE-complete problem. This problem is known to be fixed-parameter tractable if both the treewidth and alternation depth are taken as parameters. We show here that the function bounding the complexity in the paramters is provably nonelementary (assuming P is different than NP). This yields a strict hierarchy of fixed-parameter tractability inside PSPACE. As a tool for proving this result, we first prove a similar hierarchy for model checking QPTL, quantified propositional temporal logic. Finally, we show that QBF instances restricted to very slowly increasing ($\log^*$) treewidth are still PSPACE-complete.
12:00‑12:30	Martin Otto (Technische Universitaet Darmstadt) The boundedness problem for monadic universal first-order logic We consider the monadic boundedness problem for least fixed points over first-order formulae as a decision problem: Given a formula phi(X,x) in some fragment of FO, positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on phi. Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in at most one polarity (e.g., negative in all non-recursive predicates and equality). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and a reduction to the monadic second-order theory of trees.

Lunch break (12:30‑14:00)

Session 2: Concurrency (14:00‑15:30)
Chair: Christel Baier

14:00‑14:30	Marcelo Fiore (Cambridge University Computer Laboratory) Sam Staton (Cambridge University Computer Laboratory) A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics We introduce and develop a mathematical structural operational semantics for name-passing systems within the framework of nominal sets. From this model theory we extract a GSOS-like rule format for name-passing process calculi for which the induced notion of behavioural equivalence ---given by quasi-open bisimilarity--- is guaranteed to be a congruence. This work provides an analysis of the congruence properties of bisimilarity for name-passing systems, with the pi-calculus being the paradigmatic example. We ask: What is a name-passing process calculus, and when is its behavioural equivalence a congruence? We tackle these questions from a model-theoretic perspective, merging the following series of strands in semantics research: denotational models of the pi-calculus, mathematical structural operational semantics, categorical rule formats, algebraic theories for binding operators. Specifically, the paper presents the following two main developments. 1. A refinement of the mathematical structural operational semantics for name-passing systems of Fiore and Turi, by shifting from semantic universes based on functor categories to more convenient ones based on nominal sets. 2. The formalisation of a concrete syntactic rule format for name-passing process calculi designed so as to induce abstract operational rules as in the mathematical structural operational semantics of Turi and Plotkin, and hence to guarantee that bisimilarity is a congruence.
14:30‑15:00	Catuscia Palamidessi (INRIA) Vijay Saraswat (IBM) Frank D. Valencia (CNRS and LIX, Ecole Polytechnique) Björn Victor (Uppsala University) On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus We present an expressiveness study of linearity and persistence of processes. We choose the $\pi$-calculus, one of the main representative of process calculi, as a framework to conduct our study. We consider four fragments of the $\pi$-calculus. Each one singles out a natural source of linearity/persistence also present in other frameworks such Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing, or proving the non-existence, of encodings among the fragments, processes-as-formulae interpretations and reductions from Minsky machines. The fragments are: (1) The \emph{(polyadic) asynchronous} $\pi$-calculus $\api$, (2) \emph{persistent-input} $\api$ defined as $\api$ with all inputs replicated, (3) \emph{persistent-output} $\api$ defined as $\api$ with all outputs replicated, and (4) \emph{persistent} $\api$ is $\api$ with all inputs and outputs replicated. We provide compositional fully-abstract encodings, homomorphic w.r.t the parallel operator, from (1) into (2) and (3) capturing the behaviour of the source processes. In contrast, we show that it is impossible to provide such kind of encodings from (1) into (4). Nevertheless we prove that (4) is Turing-powerful. We further show that barbed-congruence is undecidable for the zero-adic version of (2), the monadic of (3) and the bi-adic of (4). In contrast, we show that it is decidable for the zero-adic versions of (3) and (4). Furthermore, we provide a compositional interpretation of the $\pi$ processes in (4) as First-Order Logic (FOL) formulae. The interpretation translates restriction and input binders into existential and universal quantifiers respectively. We illustrate how the interpretation simulates name extrusion (mobility) in FOL. We use the interpretation to characterize the standard $\pi$-calculus notion of barbed observability (reachability) as FOL entailment. We apply this characterization and classic FOL results by Bernays, Sch\"{o}nfinkel and G\"{o}del to identify decidable classes (w.r.t. barbed reachability) of infinite-state processes exhibiting meaningful mobile behaviour.
15:00‑15:30	Filippo Bonchi (Computer Science Department, University of Pisa) Ugo Montanari (Universitā di Pisa) Barbara König (IIIS, Univeristy of Duisburg-Essen) Saturated Semantics for Reactive Systems The semantics of process calculi has traditionally been specified by labelled transition systems (LTS), but with the development of name calculi it turned out that reaction rules (i.e., unlabelled transition rules) are often more natural. This leads to the question of how behavioural equivalences (bisimilarity, trace equivalence, etc.) defined for LTS can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an LTS from reaction rules in such a way that the resulting equivalences are congruences. Furthermore these equivalences should agree with the intended semantics, whenever one exists. In this paper we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and a subset of the open pi-calculus. Indeed, we prove that our equivalences are congruences and that they coincide with logical equivalence and open bisimilarity respectively, while equivalences studied in previous work are strictly finer.

Break (15:30‑16:00)

Session 3: Pushdown Systems (16:00‑18:00)
Chair: Mahesh Viswanathan

16:00‑16:30	Luke Ong (Oxford University Computing Laboratory) On model-checking trees generated by higher-order recursion schemes We prove that the modal mu-calculus model-checking problem for (ranked and ordered) node-labelled trees that are generated by order-n recursion schemes (whether safe or not, and whether homogeneously typed or not) is n-EXPTIME complete, for every n ≥ 0. It follows that the monadic second-order theories of these trees are decidable. There are three major ingredients. The first is a certain transference principle from the tree generated by the scheme -- the value tree -- to an auxiliary computation tree, which is itself a tree generated by a related order-0 recursion scheme (equivalently, a regular tree). Using innocent game semantics in the sense of Hyland and Ong, we establish a strong correspondence between paths in the value tree and traversals in the computation tree. This allows us to prove that a given alternating parity tree automaton (APT) has an (accepting) run-tree over the value tree iff it has an (accepting) traversal-tree over the computation tree. The second ingredient is the simulation of an (accepting) traversal-tree by a certain set of annotated paths over the computation tree; we introduce traversal-simulating APT as a recognising device for the latter. Finally, for the complexity result, we prove that traversal-simulating APT enjoy a succinctness property: for deciding acceptance, it is enough to consider run-trees that have a reduced branching factor. The desired bound is then obtained by analysing the complexity of solving an appropriate (finite) acceptance parity game.
16:30‑17:00	Dietrich Kuske (Universtität Leipzig) Markus Lohrey (University of Stuttgart) Monadic chain logic over iterations and applications to pushdown systems Logical properties of iterations of relational structures are studied and these decidability results are applied to the model checking of a powerful extension of pushdown systems. It is shown that the monadic chain theory of the iteration of a structure A (in the sense of Shelah and Stupp) is decidable in case the first-order theory of the structure A is decidable. This result fails if Muchnik's clone-predicate is added. A model of pushdown automata, where the stack alphabet is given by an arbitrary (possibly infinite) relational structure, is introduced. If the stack structure has a decidable first-order theory with regular reachability predicates, then the same holds for the configuration graph of this pushdown automaton. This result follows from our decidability result for the monadic chain theory of the iteration.
17:00‑17:30	Vineet Kahlon (NEC Laboratories, Princeton) Aarti Gupta (NEC Laboratories USA) An Automata-theoretic Appraoch for Model Checking Threads for LTL Properties In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads. However, we exploit the observation that, in practice, a large fraction of concurrent programs can either be modeled as Pushdown Systems communicating solely using locks or can be reduced to such systems by applying standard abstract interpretation techniques or by exploiting separation of data from control. Examples include file systems like Daisy. Moreover, standard programming practice guidelines typically recommend that programs use locks in a nested fashion. In fact, in languages like Java and C\#, locks are guaranteed to be nested. For such a framework, we show that while the model checking problem for the full-blown Linear Temporal Logic (LTL) is efficiently decidable; it remains undecidable for the non-nested case. In addition to delineating the decidability boundary for concurrent programs, our results also provide an elegant characterization, viz., nestedness of locks, for the decidability of the LTL model checking problem for threads communicating via locks.Our technique involves leveraging the new concept of Lock-constrained Multi-automata Pair (LMAP) to reduce the LTL model checking problem for a concurrent program with nested locks to those for its individual threads. This not only avoids the state explosion problem but also makes our technique provably efficient, fully automatic, sound and complete, and applicable for a broad range of correctness properties, not just reachability.
17:30‑18:00	Tachio Terauchi (University of California at Berkeley) Alex Aiken (Stanford University) On Typability for Rank-2 Intersection Types with Polymorphic Recursion We show that typability for a natural form of polymorphic recursive typing for rank-2 intersection types is undecidable. Our proof involves characterizing typability as a context free language (CFL) graph problem, which may be of independent interest, and reduction from the boundedness problem for Turing machines. We also show a property of the type system which, in conjunction with the undecidability result, disproves a misconception about the Milner-Mycroft type system. We also show undecidability of a related program analysis problem.

LICS Business Meeting (18:00‑19:00)