Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2013, held in San Diego, CA, USA in January 2013. The volume presents 29 revised refereed papers carefully selected by the program committee. The scope of the Symposium is broad and includes constructive mathematics and type theory; logic, automata and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logic; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple agent system logics; logics of proof and justification; nonmonotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; and other logics in computer science.



Compositional Reasoning for Multi-modal Logics

We provide decomposition and quotienting results for multi-modal logic with respect to a composition operator, traditionally used for epistemic models, due to van Eijck et al. (Journal of Applied Non-Classical Logics 21(3–4):397–425, 2011), that involves sets of atomic propositions and valuation functions from Kripke models. While the composition operator was originally defined only for epistemic S5 n models, our results apply to the composition of any pair of Kripke models. In particular, our quotienting result extends a specific result in the above mentioned paper by van Eijck et al. for the composition of epistemic models with disjoint sets of atomic propositions to compositions of any two Kripke models regardless of their sets of atomic propositions. We also explore the complexity of the formulas we construct in our decomposition result.
Luca Aceto, Anna Ingólfsdóttir, Cristian Prisacariu, Joshua Sack

Explicit Generic Common Knowledge

The name Generic Common Knowledge (GCK) was suggested by Artemov to capture a state of a multi-agent epistemic system that yields iterated knowledge I(ϕ): ‘any agent knows that any agent knows that any agent knows…ϕ’ for any number of iterations. The generic common knowledge of ϕ, \(\mbox{\em GCK}(\varphi)\), yields I(ϕ),
$$ \mbox{\em GCK}(\varphi)\rightarrow I(\varphi) $$
but is not necessarily logically equivalent to I(ϕ). Modal logics with GCK were suggested by McCarthy and Artemov. It has been shown that in the usual epistemic scenarios, GCK can replace the conventional common knowledge. Artemov noticed that such epistemic actions as public announcements of atomic sentences, generally speaking, yield GCK rather than the conventional common knowledge. In this paper we introduce logics with explicit GCK and show that they realize corresponding modal systems, i.e., GCK, along with the individual knowledge modalities, can be always made explicit.
Evangelia Antonakos

Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification

Relational Hoare Logic is a generalization of Hoare logic that allows reasoning about executions of two programs, or two executions of the same program. It can be used to verify that a program is robust or (information flow) secure, and that two programs are observationally equivalent. Product programs provide a means to reduce verification of relational judgments to the verification of a (standard) Hoare judgment, and open the possibility of applying standard verification tools to relational properties. However, previous notions of product programs are defined for deterministic and structured programs. Moreover, these notions are symmetric, and cannot be applied to properties such as refinement, which are asymmetric and involve universal quantification on the traces of the first program and existential quantification on the traces of the second program.
Asymmetric products generalize previous notions of products in three directions: they are based on a control-flow graph representation of programs, they are applicable to non-deterministic languages, and they are by construction asymmetric. Thanks to these characteristics, asymmetric products allow to validate abstraction/refinement relations between two programs, and to prove the correctness of advanced loop optimizations that could not be handled by our previous work. We validate their effectiveness by applying a prototype implementation to verify representative examples from translation validation and predicate abstraction.
Gilles Barthe, Juan Manuel Crespo, César Kunz

Assignment Calculus: A Pure Imperative Language

We undertake a study of imperative computation. Beginning with a philosophical analysis of the distinction between imperative and functional language features, we define a (pure) imperative language as one whose constructs are (inherently) referentially opaque. We then give a definition of a computation language by identifying desirable properties for such a language.
We present a new pure imperative computation language, Assignment Calculus AC. The main idea behind AC is based on the insight of T. Janssen that Montague’s modal operators of intension and extension, developed for the study of natural language semantics, are also useful for the semantics of programming language features such as assignments and pointers. AC consists of only four basic constructs, assignmentX: = t’, sequencet;u’, procedure formation¡t’ and procedure invocation!t’. Two interpretations are given for AC: an operational semantics and a term-rewriting system; these interpretations turn out to be equivalent.
Marc Bender, Jeffery Zucker

Multiplayer Cost Games with Simple Nash Equilibria

Multiplayer games with selfish agents naturally occur in the design of distributed and embedded systems. As the goals of selfish agents are usually neither equivalent nor antagonistic to each other, such games are non zero-sum games. We study such games and show that a large class of these games, including games where the individual objectives are mean- or discounted-payoff, or quantitative reachability, and show that they do not only have a solution, but a simple solution. We establish the existence of Nash equilibria that are composed of k memoryless strategies for each agent in a setting with k agents, one main and k − 1 minor strategies. The main strategy describes what happens when all agents comply, whereas the minor strategies ensure that all other agents immediately start to co-operate against the agent who first deviates from the plan. This simplicity is important, as rational agents are an idealisation. Realistically, agents have to decide on their moves with very limited resources, and complicated strategies that require exponential—or even non-elementary—implementations cannot realistically be implemented. The existence of simple strategies that we prove in this paper therefore holds a promise of implementability.
Thomas Brihaye, Julie De Pril, Sven Schewe

Forward Chaining for Hybrid ASP

In this paper, we define an analogue of the Forward Chaining (FC) algorithm due to Marek, Nerode, and Remmel [12] for Hybrid Answer Set Programming (H-ASP). The FC algorithm for normal logic programs takes as an input a well ordering ≺ of the non-Horn clauses of a normal logic program P and produces a stable model D  ≺  for a subprogram A  ≺  of P. It is the case that for every stable model M of P, there is a well ordering ≺ such that D  ≺  = M and A  ≺  = P. Thus the search for a stable model of P becomes a search for a well ordering ≺ such that A  ≺  = P. We show that a similar result hold in case of FC for H-ASP. H-ASP is an extension of normal logic programming or Answer Set Programming (ASP), introduced by the authors in [2] that allows users to combine ASP type rules and numerical algorithms. The MFC algorithm, introduced by the authors in [1] is a Monte Carlo algorithm that combines the FC algorithm and the Metropolis-Hastings algorithm to search for stable models of normal logic programs. We shall briefly discuss how one can produce an analogue of the MFC algorithm to search for stable models of H-ASP programs.
Alex Brik, Jeffrey B. Remmel

Effectivity Questions for Kleene’s Recursion Theorem

The present paper explores the interaction between two recursion-theoretic notions: program self-reference and learning partial recursive functions in the limit. Kleene’s Recursion Theorem formalises the notion of program self-reference: It says that given a partial-recursive function ψ p there is an index e such that the e-th function ψ e is equal to the e-th slice of ψ p . The paper studies constructive forms of Kleene’s recursion theorem which are inspired by learning criteria from inductive inference and also relates these constructive forms to notions of learnability. For example, it is shown that a numbering can fail to satisfy Kleene’s Recursion Theorem, yet that numbering can still be used as a hypothesis space when learning explanatorily an arbitrary learnable class. The paper provides a detailed picture of numberings separating various versions of Kleene’s Recursion Theorem and learnability.
John Case, Sanjay Jain, Frank Stephan

Sub-computable Bounded Pseudorandomness

This paper defines a new notion of bounded pseudorandomness for certain classes of sub-computable functions where one does not have access to a universal machine for that class within the class. In particular, we define such a version of randomness for the class of primitive recursive functions and a certain subclass of PSPACE functions. Our new notion of primitive recursive bounded pseudorandomness is robust in that there are equivalent formulations in terms of (1) Martin-Löf tests, (2) Kolmogorov complexity, and (3) martingales.
Douglas Cenzer, Jeffrey B. Remmel

Automated Support for the Investigation of Paraconsistent and Other Logics

We automate the construction of analytic sequent calculi and effective semantics for a large class of logics formulated as Hilbert calculi. Our method applies to infinitely many logics, which include the family of paraconsistent C-systems, as well as to other logics for which neither analytic calculi nor suitable semantics have so far been available.
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky

A Modal BI Logic for Dynamic Resource Properties

The logic of Bunched implications (BI) and its variants or extensions provide a powerful framework to deal with resources having static properties. In this paper, we propose a modal extension of BI logic, called DBI, which allows us to deal with dynamic resource properties. After defining a Kripke semantics for DBI, we illustrate the interest of DBI for expressing some dynamic properties and then we propose a labelled tableaux calculus for this logic. This calculus is proved sound and complete w.r.t. the Kripke semantics. Moreover, we also give a method for countermodel generation in this logic.
J. R. Courtault, D. Galmiche

Stuttering for Abstract Probabilistic Automata

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. In a series of recent papers, we proposed Abstract Probabilistic Automata (APAs), a new abstraction framework for representing possibly infinite sets of PAs. We have developed a complete abstraction theory for APAs, and also proposed the first specification theory for them. APAs support both satisfaction and refinement operators, together with classical stepwise design operators.
One of the major drawbacks of APAs is that the formalism cannot capture PAs with hidden actions – such actions are however necessary to describe behaviors that shall not be visible to a third party. In this paper, we revisit and extend the theory of APAs to such context. Our first main result takes the form of proposal for a new probabilistic satisfaction relation that captures several definitions of PAs with hidden actions. Our second main contribution is to revisit all the operations and properties defined on APAs for such notions of PAs. Finally, we also establish the first link between stochastic modal logic and APAs, hence linking an automata-based specification theory to a logical one.
Benoît Delahaye, Kim G. Larsen, Axel Legay

Call-by-Value Non-determinism in a Linear Logic Type Discipline

We consider the call-by-value λ-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent intersection types, we endow this calculus with a type system based on the so-called Girard’s second translation of intuitionistic logic into linear logic. We prove that a term is typable if and only if it is converging, and that its typing tree carries enough information to give a bound on the length of its lazy call-by-value reduction. Moreover, when the typing tree is minimal, such a bound becomes the exact length of the reduction.
Alejandro Díaz-Caro, Giulio Manzonetto, Michele Pagani

The Wadge Hierarchy of Petri Nets ω-Languages

We describe the Wadge hierarchy of the ω-languages recognized by deterministic Petri nets. This is an extension of the celebrated Wagner hierarchy which turned out to be the Wadge hierarchy of the ω-regular languages. Petri nets are an improvement of automata. They may be defined as partially blind multi-counter automata. We show that the whole hierarchy has height \(\omega^{\omega^2}\), and give a description of the restrictions of this hierarchy to every fixed number of partially blind counters.
Jacques Duparc, Olivier Finkel, Jean-Pierre Ressayre

Iterated Contraction Based on Indistinguishability

We introduce a class of set-theoretic operators on a tolerance space that models the process of minimal belief contraction, and therefore a natural process of iterated contraction can be defined. We characterize the class of contraction operators and study the properties of the associated iterated belief contraction.
Konstantinos Georgatos

A Note on Extensions: Admissible Rules via Semantics

Any intermediate logic with the disjunction property admits the Visser rules if and only if it has the extension property. This equivalence restricts nicely to the extension property up to n. In this paper we demonstrate that the same goes even when omitting the rule ex falso quod libet, that is, working over minimal rather than intuitionistic logic. We lay the groundwork for providing a basis of admissibility for minimal logic, and tie the admissibility of the Mints–Skura rule to the extension property in a stratified manner.
Jeroen Goudsmit

Subset Space vs Relational Semantics of Bimodal Logic: Bringing Out the Difference

Correspondence theory regarding the bimodal language for subset spaces can be based on a certain pseudo-monadic second-order language arising from the relevant semantics. Since the latter language is reducible to a two-sorted language of first-order predicate logic, one can apply well-established model-theoretic techniques to studying expressivity issues. In this way, a subset space analogue to a popular definability result of ordinary modal logic is proved first in this paper. On the other hand, subset spaces can easily be related to usual Kripke models, for which we have a (one-sorted) relational first-order correspondence language. Both of the concurrent correspondents are then used in the main part of the paper, where, among other things, some Goldblatt-Thomason style results as related to subset frames are proved.
Bernhard Heinemann

Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems

We combine quantified differential dynamic logic (Qd \(\mathcal{L}\)) for reasoning about the possible behavior of distributed hybrid systems with temporal logic for reasoning about the temporal behavior during their operation. Our logic supports verification of temporal and non-temporal properties of distributed hybrid systems and provides a uniform treatment of discrete transitions, continuous evolution, and dynamic dimensionality-changes. For our combined logic, we generalize the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of Qd \(\mathcal{L}\) for distributed hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of temporal behavior of distributed hybrid systems to non-temporal reasoning, and prove that we obtain a complete axiomatization relative to the non-temporal base logic Qd \(\mathcal{L}\). Using this calculus, we analyze temporal safety properties in a distributed air traffic control system where aircraft can appear dynamically.
Ping Hou, Hao Zheng

Computational Hardness of Validity in Probability Logic

We consider the complexity of validity in ε-logic, a probability logic introduced by Terwijn. We prove that the set of valid formulas is \(\mathrm{\Pi}^1_1\)-hard, improving a previous undecidability result by Terwijn.
Rutger Kuyper

Update as Evidence: Belief Expansion

We introduce a justification logic with a novel constructor for evidence terms, according to which the new information itself serves as evidence for believing it. We provide a sound and complete axiomatization for belief expansion and minimal change and explain how the minimality can be graded according to the strength of reasoning. We also provide an evidential analog of the Ramsey axiom.
Roman Kuznets, Thomas Studer

Separating the Fan Theorem and Its Weakenings

Varieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which suffices to separate all of the as yet identified fan theorems.
Robert S. Lubarsky, Hannes Diener

The Logic of Uncertain Justifications

In Artemov’s Justification Logic, one can make statements interpreted as “t is evidence for the truth of formula F.” We propose a variant of this logic in which one can say “I have degree r of confidence that t is evidence for the truth of formula F.” After defining both an axiomatic approach and a semantics for this Logic of Uncertain Justifications, we will prove the usual soundness and completeness theorems.
Bob Milnikel

Justifications, Awareness and Epistemic Dynamics

The paper introduces a new kind of models for the logic of proofs LP, the group justification models. While being an elaboration of Fitting models, the group justification models are a special case of the models of general awareness. Soundness and completeness results of LP with respect to the new semantics are established. The paper also offers an interpretation of the group models, which pertains to awareness and group epistemic dynamics.
Igor Sedlár

Normal Forms for Multiple Context-Free Languages and Displacement Lambek Grammars

We introduce a new grammar formalism, the displacement context-free grammars, which is equivalent to well-nested multiple context-free grammars. We generalize the notions of Chomsky and Greibach normal forms for these grammars and show that every language without the empty word generated by a displacement context-free grammar can be also generated by displacement Lambek grammars.
Alexey Sorokin

Constructive Polychronous Systems

The synchronous paradigm provides a logical abstraction of time for reactive system design which allows automatic synthesis of embedded programs that behave in a predictable, timely and reactive manner. According to the synchrony hypothesis, a synchronous model reacts to input events and generates outputs that are immediately made available. But even though synchrony greatly simplifies design of complex systems, it often leads to rejecting models when data dependencies within a reaction are ill-specified, leading to causal cycles. Constructivity is a key property to guarantee that the output during each reaction can be algorithmically determined. Polychrony deviates from perfect synchrony by using a partially ordered or relational model of time. It captures the behaviors of (implicitly) multi-clocked data-flow networks and can analyze and synthesize them to GALS systems or to Kahn process networks (KPNs). In this paper, we provide a unified constructive semantic framework, using structural operational semantics, which captures the behavior of both synchronous modules and multi-clocked polychronous processes. Along the way, we define the very first operational semantics of Signal.
Jean-Pierre Talpin, Jens Brandt, Mike Gemünde, Klaus Schneider, Sandeep Shukla

On Tolerance Analysis of Games with Belief Revision

Aumann’s Rationality Theorem claims that in perfect information games, common knowledge of rationality yields backward induction (BI). Stalnaker argued that in the belief revision setting, BI does not follow from Aumann’s assumptions. However, as shown by Artemov, if common knowledge of rationality is understood in the robust sense, i.e., if players do not forfeit their knowledge of rationality even hypothetically, then BI follows. A more realistic model would bound the number of hypothetical non-rational moves by player i that can be tolerated without revising the belief in i’s rationality on future moves. We show that in the presence of common knowledge of rationality, if n hypothetical non-rational moves by any player are tolerated, then each game of length less than 2n + 3 yields BI, and that this bound on the length of model is tight for each n. In particular, if one error per player is tolerated, i.e., n = 1, then games of length up to 4 are BI games, whereas there is a game of length 5 with a non-BI solution.
Çağıl Taşdemir

Temporalizing Modal Epistemic Logic

Timed Modal Epistemic Logic, tMEL, is a newly introduced logical framework for reasoning about the modeled agent’s knowledge. The framework, derived from the study of Justification Logic, is adapted from the traditional Modal Epistemic Logic, MEL, to serve as a logically non-omniscient epistemic logic and dealing with problems where the temporal constraint is an unavoidable factor. In this paper we will give a semantic proof for the formal connection between MEL and tMEL, the Temporalization Theorem, which states that every MEL theorem can be turned into a tMEL theorem if suitable time labels can be found for each knowledge statement involved in the MEL theorem. As a result, the proof also gives us a better understanding of the semantics on the both sides of the theorem.
Ren-June Wang

Contextual Natural Deduction

This paper defines the contextual natural deduction calculus \(\textbf{ND}^\textbf{c}\) for the implicational fragment of intuitionistic logic. \(\textbf{ND}^\textbf{c}\) extends the usual natural deduction calculus (here called \(\textbf{ND}\)) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. In analogy to the Curry-Howard isomorphism between \(\textbf{ND}\) and the simply-typed λ-calculus, an extension of the λ-calculus, here called λ c -calculus, is defined in order to provide compact proof-terms for \(\textbf{ND}^\textbf{c}\) proofs. Soundness and completeness of \(\textbf{ND}^\textbf{c}\) with respect to \(\textbf{ND}\) are proven by defining translations of proofs between these calculi. Furthermore, some \(\textbf{ND}^\textbf{c}\)-proofs are shown to be quadratically smaller than the smallest \(\textbf{ND}\)-proofs of the same theorems.
Bruno Woltzenlogel Paleo

Conservatively Approximable Functions

In the study of computable functions on the Cantor space 2, it is well-known that the image of such a function is an effectively closed set, or \(\Pi^0_1\) class and in fact a decidable closed set. Here a closed subset Q of the Cantor space is decidable if the set of finite strings w which have an extension in Q is a computable set. It was shown recently by Cenzer, Dashti and King that the set of itineraries of a computable function is also a decidable closed set. Now the set of itineraries of a continuous function is always a subshift, meaning that it is closed under prefixes. It was also shown that any decidable shift is the set of itineraries of some computable function on 2. This paper defines the new notion of a conservatively approximable function on the Cantor space in order to have a family of functions whose images, and itineraries, can be arbitrary \(\Pi^0_1\) classes.
Sebastian Wyman

Self-referentiality in the Brouwer–Heyting–Kolmogorov Semantics of Intuitionistic Logic

The intended provability semantics of Intuitionistic Propositional Logic IPC (also called Brouwer–Heyting–Kolmogorov semantics) has been formalized within Gödel-Artemov’s framework. According to this approach, IPC is embedded in modal logic S4 by Gödel embedding and S4 is realized in Artemov’s Logic of Proofs LP which has a provability interpretation in Peano Arithmetic. Artemov’s realization of S4 in LP uses self-referential LP-formulas of the form \(t\!\!:\!\!\phi(t)\), namely, ‘t is a proof of a formula φ containing t itself.’ Kuznets showed that this is not avoidable by offering S4-theorems that cannot be realized without using self-referential LP-formulas. This paper extends Kuznets’ method to find IPC-theorems that call for direct self-referentiality in LP. Roughly speaking, examples include double-negations of tautologies that are not IPC-theorems, e.g., \(\neg\neg(\neg\neg p\!\rightarrow\! p)\), and there are also examples in the purely implicational fragment IPC  → . This suggests that the Brouwer–Heyting–Kolmogorov semantics of intuitionistic logic is intrinsically self-referential.
Junhua Yu


Weitere Informationen

Premium Partner