LICS on Tuesday, August 15th

Invited Talk (09:00‑10:00)
Chair: Radha Jagadeesan

09:00‑10:00

Andy Gordon (Microsoft Research) Provable Implementations of Security Protocols [ppt] Proving cryptographic security protocols has been a challenge ever since Needham and Schroeder threw down the gauntlet in their pioneering 1978 paper on authentication protocols: "The need for techniques to verify the correctness of such protocols is great, and we encourage those interested in such problems to consider this area." By now, there is a wide range of informal and formal methods that can catch most design errors. Still, as in other areas of software, the trouble is that while practitioners are typically happy for researchers to write formal models of their natural language specifications and to apply design principles, they are reluctant to do so themselves. In practice, specifications tend to be partial and ambiguous, and the implementation code is the closest we get to a formal description of most protocols. This motivates the subject of my talk: the relatively new enterprise of adapting formal methods for security protocols to work on code instead of abstract models. The goal is to lower the practical cost of security protocol verification by eliminating the need to write a separate formal model. I will describe current tools that partially address the problem, and discuss what remains to be done.

Break (10:00‑10:30)

Session 9: Timed and Stochastic Systems (10:30‑12:00)
Chair: Mahesh Viswanathan

10:30‑11:00	Tomas Brazdil (Masaryk University) Vaclav Brozek (Masaryk University) Vojtech Forejt (Masaryk University) Antonin Kucera (Masaryk University) Stochastic Games with Branching-Time Winning Objectives We consider stochastic turn-based games where the winning objectives are given by formulae of the branching-time logic PCTL. These games are generally not determined and winning strategies may require memory and/or randomization. Our main results concern history-dependent strategies. In particular, we show that the problem whether there exists a history-dependent winning strategy in $1 1/2$-player games is highly undecidable, even for objectives formulated in the $L(F^{=5/8},F^{=1},F^{>0},G^{=1})$ fragment of PCTL. On the other hand, we show that the problem becomes decidable (and in fact EXPTIME-complete) for the qualitative $L(F^{=1},F^{>0},G^{=1})$ fragment of PCTL, where winning strategies require only a finite memory. This result is tight in the sense that winning strategies for $L(F^{=1},F^{>0},G^{=1},G^{>0})$ objectives already require infinite memory.
11:00‑11:30	Dexter Kozen (Cornell University) Coinductive Proof Principles for Stochastic Processes We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. We illustrate the use of the rule in deriving properties of a simple coin-flip process.
11:30‑12:00	Patricia Bouyer (LSV - CNRS & ENS de Cachan) Thomas Brihaye (Universite de Mons-Hainaut) Fabrice Chevalier (LSV - CNRS & ENS de Cachan) Control in o-minimal hybrid systems In this paper, we consider the control of general hybrid systems. In this context we show that time-abstract bisimulation is not adequate for solving such a problem. That is why we considered an other equivalence, namely the suffix equivalence based on the encoding of trajectories through words. We show that this suffix equivalence is in general a correct abstraction for control problems. We apply this result to o-minimal hybrid systems, and get decidability and computability results in this framework.

Session 10: Short Presentations 1 (12:00‑12:30)
Chair: Mahesh Viswanathan

12:00‑12:10	Murray Patterson (Simon Fraser University) Yongmei Liu (Simon Fraser University) Eugenia Ternovska (Simon Fraser University) Arvind Gupta (Simon Fraser University) Grounding for Model Expansion in k-Guarded Formulas In [Mitchell and Ternovska, LCC'05, Mitchell and Ternovska, AAAI'05], the authors propose a constraint programming framework based on classical logic extended with inductive definitions. They formulate a search problem as the problem of model expansion (MX), which is model checking for existential SO where the goal is to find a witness for the existentially quantified predicates. Their long-term goal is to produce practical tools to solve combinatorial search problems, especially those in NP. In this framework, the problem is encoded in a logic, an instance of the problem is represented by a finite structure, and a solver generates solutions to the problem. This approach relies on propositionalisation of high-level specifications, and on the efficiency of modern SAT solvers. We propose an efficient algorithm which combines grounding with partial evaluation. Since the MX framework is based on classical logic, we are able to take advantage of known results for the so-called guarded fragments and their generalizations. In the case of k-guarded formulas, the algorithm performs much better than naive grounding by relying on connections between k-guarded formulas and tree decompositions.
12:10‑12:20	Jørgen Villadsen (Computer Science, Roskilde University) Nominalization in Intensional Type Theory Paul C. Gilmore's Intensional Type Theory (Journal of Symbolic Logic 2001) is motivated by a nominalist interpretation of higher order predication and provides a logical foundation of mathematics. We explore the nominalization using a sequent calculus for ITT and relate the approach to works on transfinite types.
12:20‑12:30	Leona F. Fass (Carmel-bt-the-Sea) A Logical Look at Agents’ Problem-Solving on the Semantic Web The emergent Semantic Web (SWeb) is an enhancement of the current Web, including semantic information “understandable” by Web-navigating (software) agents. With the SWeb, agents may make logical decisions, choose actions and interact within configurations that achieve specified goals. Motivated by logic-based research of SWeb practitioners we take an automata-theoretic view of agents and the SWeb. To us, configuring SWeb agents to solve complex problems is synthesis of behavioral realizations. Tasks to-be-fulfilled and goals to-be-achieved on the SWeb are behaviors to-be-realized. With this approach we obtain theoretical results that can ground the real-world results obtained in practice. Adapting classical automata theory techniques for SWeb agents’ problem-solving, we show that “optimal” agent configurations can be found to achieve specified goals. Augmenting useful theoretical results we note real-world constraints and considerations. E.g., completeness and termination problems related to SWeb problem-solving are a consequence of the enormity and dynamic nature of the domain, but with a “local closed world” view, problems may be solved adequately. We illustrate a successful theoretically-designed agent configuration that can be modified to achieve changing human-specified behavioral goals. We also describe cases where real-world events prove that no problem-solving SWeb agent configuration can ever be good enough. We conclude that logic-based configurations of agents on the SWeb can reduce much human effort and solve many problems with perfect or “adequate” goal realizations. But we are relieved to provide an additional result: humans cannot be replaced completely.

Lunch break (12:30‑14:00)

Session 11: Verification (14:00‑15:30)
Chair: Stephan Kreutzer

14:00‑14:30	Thomas Ball (Microsoft Research) Orna Kupferman (Hebrew University) An Abstraction-Refinement Framework for Multi-Agent Systems Abstraction is a key technique for reasoning about systems with very large or even infinite state spaces. When a system is composed of reactive components, the interaction between the components is modeled by a multi-player game and verification corresponds to finding winners in the game. We describe an abstraction-refinement framework for multi-player games, with respect to specifications in the alternating mu-calculus (AMC). Our framework is based on abstract alternating transition systems (AATS). Each agent in an AATS has transitions that over-approximate its power and transitions that under-approximate its power. We define the framework, define a 3-valued semantics for AMC formulas in an AATS, study the model-checking problem, define an abstraction preorder between ATSs, suggest a refinement procedure (in case model checking returns an indefinite answer) and study the completeness of the framework. For the case of predicate abstraction, we show how such reasoning can be automated with a theorem prover. Abstractions of multi-player games have been studied in the past. Our main contribution with respect to earlier work is that we study general (rather than only turn-based) ATSs, we add a refinement procedure on top of the model-checking procedure, and our abstraction preorder is parameterized by a set of agents.
14:30‑15:00	Daniele Varacca (Imperial College London) Hagen Voelzer (University of Luebeck) Temporal logics and model checking for fairly correct systems We motivate and study a generic relaxation of correctness of reactive and concurrent systems with respect to a temporal specification. We define a system to be fairly correct if there exists a fairness assumption under which it satisfies its specification. Equivalently, a system is fairly correct if the set of runs satisfying the specification is large from a topological point of view, i.e., it is a \emph{co-meager} set. We compare topological largeness with its more popular sibling, probabilistic largeness, where a specification is probabilistically large if the set of runs satisfying the specification has probability 1. We show that topological and probabilistic largeness of \omega-regular specifications coincide in finite-state Markov chains. As a corollary, we show that, for specifications expressed in LTL or by B\"uchi automata, checking that a finite-state system is fairly correct has the same complexity as checking that it is correct. Finally we study variants of the logics CTL and CTL*, where the ``for all runs'' quantifier is replaced by a ``for a large set of runs'' quantifier. We show that the model checking complexity for these variants is the same as for the original logics.
15:00‑15:30	Sharon Shoham (Technion - Israel Institute of Technology) Orna Grumberg (Prof. Dept. of Computer Science, Technion) 3-Valued Abstraction: More Precision at Less Cost This paper investigates both the \emph{precision} and the model checking \emph{efficiency} of abstract models designed to preserve branching time logics w.r.t. a 3-valued semantics. Current abstract models use ordinary transitions to over approximate the concrete transitions, while they use hyper transitions to under approximate the concrete transitions. In this work we refer to precision measured w.r.t. the choice of abstract states, independently of the formalism used to describe abstract models. We show that current abstract models do not allow maximal precision. We suggest a new class of models and a construction of an abstract model which is \emph{most precise} w.r.t. to \emph{any} choice of abstract states. As before, the construction of such models might involve an exponential blowup, which is inherent by the use of hyper transitions. We therefore suggest an efficient algorithm in which the abstract model is constructed \emph{during} model checking, by need. Our algorithm achieves maximal precision w.r.t. the given property while remaining quadratic in the number of abstract states. To complete the picture, we incorporate it into an abstraction-refinement framework.

Break (15:30‑16:00)

Session 12: Approximations (16:00‑17:00)
Chair: Victor Dalmau

16:00‑16:30

Anuj Dawar (University of Cambridge) Martin Grohe (Humboldt University Berlin) Stephan Kreutzer (Humboldt University Berlin) Nicole Schweikardt (Humboldt University Berlin) Approximation Schemes for First-Order Definable Optimization Problems Let F(X) be a first-order formula in the language of graphs that has a free set variable X, and assume that X only occurs positively in F(X). Then a natural minimization problem associated with F(X) is to find, in a given graph G, a vertex set S of minimum size such that G satisfies F(S). Similarly, if X only occurs negatively in X then F(X) defines a maximization problem. Many well-known optimization problems are first-order definable in this sense, for example, MINIMUM DOMINATING SET or MAXIMUM INDEPENDENT SET. We prove that for each class C of graphs with excluded minors, in particular for each class of planar graphs, the restriction of a first-order definable optimization problem to the class C has a polynomial time approximation scheme. A crucial building block of the proof of this approximability result is a version of Gaifman's locality theorem for formulas positive in a set variable. This result may be of independent interest.

16:30‑17:00

Eldar Fischer (Technion - Israel Institute of Technology) Frederic Magniez (CNRS - LRI) Michel de Rougemont (LRI - Universite Paris 2) Approximate Satisfiability and Equivalence We relax the classical satisfiability $U \models F$ between a finite structure $U$ of a class $\mathbf{K}$ and a formula $F$, to a notion of $\eps$-satisfiability $U \models_{\eps} F$, and the classical equivalence $F_1 \equiv F_2$ between two formulas $F_1$ and $F_2$, to $\eps$-equivalence $F_1 \equiv_{\eps} F_2$ for $\eps>0$, inspired by Property Testing. We consider the class of strings and trees with the edit distance with moves, and show that these approximate notions can be efficiently decided. We use a statistical embedding of words (resp. trees) into $\ell_1$, which generalizes the original Parikh mapping, obtained by sampling $O(f(\eps))$ finite samples of the words (resp. trees). We give a tester for equality and membership in any regular language, in time independent of the size of the structure. Using our geometrical embedding, we can also test the equivalence between two regular properties on words, defined by Monadic Second Order formulas. Our equivalence tester has polynomial time complexity in the size of the automaton (or regular expression), for a fixed $\eps$, whereas the exact version of the equivalence problem is PSPACE-complete. Last, we extend the geometric embedding, and hence the tester algorithms, to infinite regular languages and to context-free languages. For context-free languages, the equivalence tester has an exponential time complexity, whereas the exact version is undecidable.

Session 13: Short Presentations 2 (17:00‑17:40)
Chair: Victor Dalmau

17:00‑17:10	Julian Zinn (University of Houston) Rakesh Verma (University of Houston) A Polynomial-time Algorithm for Uniqueness of Normal Forms of Linear Shallow Term Rewrite Systems Term rewrite systems are useful in many areas of computer science. Two especially important areas are in providing decision procedures for the word problem of some algebraic systems and in rule-based programming. One of the most studied properties of rewrite systems is confluence, which implies that normal forms are unique. Uniqueness of normal forms is an interesting property in its own right, since confluence can be too strong a requirement in some applications. Uniqueness of normal forms is undecidable in general. This paper develops a polynomial-time algorithm for the uniqueness of normal forms problem for the class of linear shallow term rewrite systems.
17:10‑17:20	Aaron Hunter (Simon Fraser University) Non-Closure Results for First-Order Spectra The spectrum of a first-order sentence is the set of cardinalities of its finite models. Given a spectrum S and a function f on natural numbers, it is natural to ask if the image f({\cal S}) is also a spectrum. There are some established techniques for proving affirmative answers to such questions, but there has been comparatively little work on proving negative answers. In this paper, we briefly discuss some of our current work on the use of diagonalization to prove non-closure results for spectra.
17:20‑17:30	Detlef Kaehler (University of Kiel) Ralf Kuesters (Christian-Albrechts-Universität zu Kiel) Thomas Wilke (University of Kiel) A Dolev-Yao-based Definition of Abuse-free Protocols We propose a Dolev-Yao-based definition of abuse freeness for optimistic contract-signing protocols which, unlike other definitions, incorporates a rigorous notion of what it means for an outside party to be convinced by a dishonest party that it has the ability to determine the outcome of the protocol with an honest party, i.e., to determine whether it will obtain a valid contract itself or whether it will prevent the honest party from obtaining a valid contract. Our definition involves a new notion of test (inspired by static equivalence) which the outside party can perform. We show that an optimistic contract-signing protocol proposed by Asokan, Shoup, and Waidner is abusive and that a protocol by Garay, Jakobsson, and MacKenzie is abuse-free according to our definition. Our analysis is based on a synchronous concurrent model in which parties can receive several messages at the same time. This results in new vulnerabilities of the protocols depending on how a trusted third party reacts in case it receives abort and resolve requests at the same time.
17:30‑17:40	Guillaume Burel (École Normale Supérieure de Lyon - LORIA) Claude Kirchner (LORIA - INRIA Lorraine) An Abstract Completion Procedure for Cut Elimination in Deduction Modulo Deduction Modulo implements Poincaré's principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction modulo has been shown to be logically equivalent to first-order logic, proofs in such systems are quite different and dramatically simpler with one price: cut elimination may not hold anymore. Indeed, to recover this crucial property, computation rules can be added following the classical idea of completion a la Knuth and Bendix on terms. But of course in this case the objects are much more elaborated and it becomes essential to use an abstract framework which in our case is the abstract canonical inference one. We show how, under appropriate hypothesis, the sequent calculus modulo can be seen as an instance of abstract canonical systems and that therefore, cuts correspond to critical proofs that abstract completion allows us to eliminate. In addition to a deeper understanding of the interaction between deduction and computation and of the expressive power of abstract canonical systems, this provides a mechanical way to transform a sequent calculus modulo a given proposition rewrite system into an equivalent one having the cut elimination property, therefore extending in a significant way the applicability of mechanised proof search in deduction modulo.