

FLoC MEETINGS PROGRAM FACILITIES SEATTLE ORGANIZATION MISCELLANEOUS OUTOFDATE 
LICS on Tuesday, August 15th
Invited Talk (09:00‑10:00)

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. 
10:30‑11:00  Tomas Brazdil (Masaryk University) Vaclav Brozek (Masaryk University) Vojtech Forejt (Masaryk University) Antonin Kucera (Masaryk University) Stochastic Games with BranchingTime Winning Objectives We consider stochastic turnbased games where the winning objectives are given by formulae of the branchingtime logic PCTL. These games are generally not determined and winning strategies may require memory and/or randomization. Our main results concern historydependent strategies. In particular, we show that the problem whether there exists a historydependent 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 EXPTIMEcomplete) 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 recursivelydefined 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 coinflip process. 
11:30‑12:00  Patricia Bouyer
(LSV  CNRS & ENS de Cachan) Thomas Brihaye (Universite de MonsHainaut) Fabrice Chevalier (LSV  CNRS & ENS de Cachan) Control in ominimal hybrid systems In this paper, we consider the control of general hybrid systems. In this context we show that timeabstract 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 ominimal hybrid systems, and get decidability and computability results in this framework. 
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 kGuarded 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 longterm 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 highlevel 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 socalled guarded fragments and their generalizations. In the case of kguarded formulas, the algorithm performs much better than naive grounding by relying on connections between kguarded 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
(CarmelbttheSea) A Logical Look at Agents’ ProblemSolving on the Semantic Web The emergent Semantic Web (SWeb) is an enhancement of the current Web, including semantic information “understandable” by Webnavigating (software) agents. With the SWeb, agents may make logical decisions, choose actions and interact within configurations that achieve specified goals. Motivated by logicbased research of SWeb practitioners we take an automatatheoretic view of agents and the SWeb. To us, configuring SWeb agents to solve complex problems is synthesis of behavioral realizations. Tasks tobefulfilled and goals tobeachieved on the SWeb are behaviors toberealized. With this approach we obtain theoretical results that can ground the realworld results obtained in practice. Adapting classical automata theory techniques for SWeb agents’ problemsolving, we show that “optimal” agent configurations can be found to achieve specified goals. Augmenting useful theoretical results we note realworld constraints and considerations. E.g., completeness and termination problems related to SWeb problemsolving 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 theoreticallydesigned agent configuration that can be modified to achieve changing humanspecified behavioral goals. We also describe cases where realworld events prove that no problemsolving SWeb agent configuration can ever be good enough. We conclude that logicbased 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. 
14:00‑14:30  Thomas Ball
(Microsoft Research) Orna Kupferman (Hebrew University) An AbstractionRefinement Framework for MultiAgent 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 multiplayer game and verification corresponds to finding winners in the game. We describe an abstractionrefinement framework for multiplayer games, with respect to specifications in the alternating mucalculus (AMC). Our framework is based on abstract alternating transition systems (AATS). Each agent in an AATS has transitions that overapproximate its power and transitions that underapproximate its power. We define the framework, define a 3valued semantics for AMC formulas in an AATS, study the modelchecking 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 multiplayer games have been studied in the past. Our main contribution with respect to earlier work is that we study general (rather than only turnbased) ATSs, we add a refinement procedure on top of the modelchecking 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{comeager} 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 \omegaregular specifications coincide in finitestate Markov chains. As a corollary, we show that, for specifications expressed in LTL or by B\"uchi automata, checking that a finitestate 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) 3Valued 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 3valued 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 abstractionrefinement framework. 
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 FirstOrder Definable Optimization Problems Let F(X) be a firstorder 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 wellknown optimization problems are firstorder 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 firstorder 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 PSPACEcomplete. Last, we extend the geometric embedding, and hence the tester algorithms, to infinite regular languages and to contextfree languages. For contextfree languages, the equivalence tester has an exponential time complexity, whereas the exact version is undecidable. 
17:00‑17:10  Julian Zinn (University of Houston) Rakesh Verma (University of Houston) A Polynomialtime 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 rulebased 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 polynomialtime 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) NonClosure Results for FirstOrder Spectra The spectrum of a firstorder 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 nonclosure results for spectra. 
17:20‑17:30  Detlef Kaehler (University of Kiel) Ralf Kuesters (ChristianAlbrechtsUniversität zu Kiel) Thomas Wilke (University of Kiel) A DolevYaobased Definition of Abusefree Protocols We propose a DolevYaobased definition of abuse freeness for optimistic contractsigning 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 contractsigning protocol proposed by Asokan, Shoup, and Waidner is abusive and that a protocol by Garay, Jakobsson, and MacKenzie is abusefree 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 firstorder 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. 