- Andreas Abel and Ralph Matthes
- Fixed Points of Type Constructors and Primitive Recursion
- For nested or heterogeneous datatypes, terminating recursion schemes
considered so far have been instances of iteration, excluding efficient
definitions of fixed-point unfolding. Two solutions of this problem are
proposed: The first one is a system with equi-recursive non-strictly
positive type operators of arbitrary finite kinds, where fixed-point
unfolding is computationally invisible due to its treatment on the level
of type equality. Positivity is ensured by a polarized kinding system, and
strong normalization is proven by a model construction based on saturated
sets. The second solution is a formulation of primitive recursion for
arbitrary type constructors of any rank. Although without positivity
restriction, the second system embeds — even operationally —
into the first one.
- Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal
Zilio, and Line Jakubiec
- A Functional Scenario for Bytecode Verification of Resource
Bounds
- We
consider a scenario where (functional) programs in pre-compiled form
are exchanged among untrusted parties. Our contribution is a system of
annotations for the code that can be verified at load time so as to
ensure bounds on the time and space resources required for its
execution, as well as to guarantee the usual integrity properties.
Specifically, we define a simple stack machine for a first-order
functional language and show how to perform type, size, and termination
verifications at the level of the bytecode of the machine. In
particular, we show that a combination of size verification based on
quasi-interpretations and of termination verification based on
lexicographic path orders leads to an explicit bound on the space
required for the execution.
- Marcelo Arenas, Pablo Barceló, and Leonid Libkin
- Game-based Notions of Locality over Finite Models
- Locality notions in logic say that the truth value of a formula
can be determined locally, by looking at the isomorphism type of a
small neighborhood of its free variables. Such notions have proved to
be useful in many applications. They all, however, refer to isomorphism of
neighborhoods, which most local logics cannot test. A more relaxed notion
of locality says that the truth value of a formula is determined
by what the logic itself can say about that small neighborhood. Or,
since most logics are characterized by games, the truth value of a
formula is determined by the type, with respect to a game, of that small
neighborhood. Such game-based notions of locality can often be applied
when traditional isomorphism-based locality cannot. Our goal is to study
game-based notions of locality. We work with an abstract view of games
that subsumes games for many logics. We look at three, progressively
more complicated locality notions. The easiest requires only very mild
conditions on the game and works for most logics of interest. The
other notions, based on Hanf's and Gaifman's theorems, require more
restrictions. We state those restrictions and give examples of logics
that satisfy and fail the respective game-based notions of locality.
- Alessandro Avellone, Camillo Fiorentini, Guido
Fiorino, and Ugo Moscato
- An Efficent Implementation of a Tableau Calculus for a Logic with
a Constructive Negation
- A tableau calculus for a logic with constructive negation and an
implementation of the related decision procedure is presented. This logic
is an extension of Nelson logic and it has been used in the framework of
program verification and timing analysis of combinatorial circuits. The
decision procedure is tailored to shrink the search space of proofs and
it is proved correct by using a semantical technique and it has been
implemented in C++ language.
- Mikolaj Bojanczyk
- A Bounding Quantifier
- The logic MSOL+B is defined, by extending monadic
second-order logic on the infinite binary tree with a new bounding
quantifier B. In this logic, a formula
BX.φ(X)
states that there is a finite bound on the size of sets satisfying
φ(X). Satisfiability is proved decidable for two fragments of
MSOL+B: formulas of the form ¬BX.φ(X),
with φ a B-free formula; and formulas built from
B-free formulas by nesting B, ∃, ∨
and ∧.
- Krishnendu Chatterjee,
Rupak Majumdar, and Marcin Jurdzinski
- On Nash Equilibria in Stochastic Games
- We study infinite stochastic games played by n-players on a
finite graph with goals given by sets of infinite traces. The games
are stochastic (each player simultaneously and independently
chooses an action at each round, and the next state is determined
by a probability distribution depending on the current state and the
chosen actions), infinite (the game continues for an infinite
number of rounds), nonzero sum (the players' goals are not
necessarily conflicting), and undiscounted. We show that if each
player has a reachability objective, that is, if the goal for
each player i is to visit some subset Ri
of the states, then
there exists an ε-Nash equilibrium in memoryless strategies,
for every ε>0. We study the complexity of finding such Nash
equilibria. Given an n-player reachability game, we show for every
fixed ε, the value of some memoryless ε-Nash equilibrium
can be ε-approximated in NP. However, for a vector of values
(v1,...,vn),
it is NP-complete to determine if there exists a
pure, memoryless ε-Nash equilibrium where each player gets payoff
at least vi. Our techniques for general nonzero
sum games also yield NP ∩ coNP ε-approximation
algorithms for zero-sum reachability
games, improving the previously known EXPTIME bound. We study the important
subclass of n-player perfect-information or turn-based
probabilistic games, where at each state at most one player has a
nontrivial choice of moves. For turn-based probabilistic games, we show
the existence of ε-Nash equilibria in pure strategies for
games where the objective of player i is a Borel set
Bi of
infinite traces. For the special case of ω-regular objectives,
we show exact Nash equilibria exist, and can be computed in NP when the
ω-regular objectives are expressed as parity objectives.
- Agata Ciabattoni
- Automated Generation of Analytic Calculi for Logics with
Linearity
- We show how to automatically generate analytic hypersequent
calculi for a large class of logics containing the linearity axiom
(lin) (A → B) ∨ (B → A) starting from existing analytic calculi for
the corresponding logics without (lin). As a corollary, we define an
analytic hypersequent calculus for Strict Monoidal T-norm based Logic
SMTL.
- Andrés Cordón-Franco, Alejandro
Fernández-Margarit, and F. Félix Lara-Martín
- Provably Total Primitive Recursive Functions: Theories with
Induction
-
A natural example of a function algebra is R(T), the class of
provably total computable functions (p.t.c.f.) of a theory T in the
language of first order Arithmetic. In this paper a simple
characterization of that kind of function algebras is obtained. This
provides a useful tool for studying the class of primitive recursive
functions in R(T). We prove that this is the class of p.t.c.f. of
the theory axiomatized by the induction scheme restricted to (parameter
free) Δ1(T)-formulas
(i.e., Σ1-formulas which are equivalent in
T to Π1-formulas). Moreover, if T is a sound theory and
proves that exponentiation is a total function, we characterize the
class of primitive recursive functions in R(T) as a function
algebra described in terms of bounded recursion (and composition).
Extensions of this result are related to open problems on complexity
classes. We also discuss an application to the problem on the
equivalence between (parameter free) Σ1-collection and
(uniform) Δ1-induction schemes in Arithmetic. The
proofs lean upon axiomatization and conservativeness properties of the
scheme of Δn+1(T)-induction and its parameter
free version.
- Jeremy E. Dawson and Rajeev Goré
- A General Theorem on Termination of Rewriting
- We re-express our theorem on the strong-normalisation
of display calculi
as a theorem about the well-foundedness of a certain ordering on
first-order terms, thereby allowing us to prove the termination of
systems of rewrite rules. We first show how to use our theorem to prove
the well-foundedness of the lexicographic ordering, the multiset
ordering and the recursive path ordering. Next, we give examples of
systems of rewrite rules which cannot be handled by these methods but
which can be handled by ours. Finally, we show that our method can also
prove the termination of the Knuth-Bendix ordering and of dependency
pairs.
- Philippe de Groote and Sylvain Salvati
- Higher-order Matching in the Linear λ-calculus with
Pairing
-
We prove that higher-order matching in the linear λ-calculus
with pairing is decidable. We also establish its NP-completeness under
the assumption that the right-hand side of the equation to be solved is
given in normal form.
- Pietro Di Gianantonio
- Structures for Multiplicative Cyclic Linear Logic: Deepness vs
Cyclicity
-
The aim of this work is to give an alternative presentation for the
multiplicative fragment of Yetter's cyclic linear logic. The new
presentation is inspired by the calculus of structures, and has the
interesting feature of avoiding the cyclic rule. The main point in
this work is to show how cyclicity can be substituted by deepness,
i.e., the possibility of applying an inference rule at any point of
a formula. We finally derive, through a new proof technique, the
cut elimination property of the calculus.
- E. Allen Emerson and Vineet Kahlon
- Parameterized Model Checking of Ring-based Message Passing
Systems
-
The Parameterized Model Checking Problem (PMCP) is to decide whether a
temporal property holds for a uniform family of systems comprised of
finite, but arbitrarily many, copies of a template process.
Unfortunately, it is undecidable in general. In this paper, we consider
the PMCP for systems comprised of processes arranged in a ring that
communicate by passing messages via tokens whose values can be updated
at most a bounded number of times. Correctness properties are expressed
using the stuttering-insensitive temporal logic LTL\X. For
bidirectional rings we show how to reduce reasoning about rings with an
arbitrary number of processes to rings with up to a certain finite
“cutoff” number of processes. This immediately yields
decidability of the PMCP at hand. We go on to show that for
unidirectional rings small cutoffs can be achieved, making the decision
procedure provably efficient. As example applications, we consider
protocols for the leader election problem.
- Harald Ganzinger and Konstantin Korovin
- Integrating Equational Reasoning into Instantiation-based Theorem
Proving
-
In this paper we present a method for integrating equational reasoning
into instantiation-based theorem proving. The method employs a
satisfiability solver for ground equational clauses together with an
instance generation process based on an ordered paramodulation type
calculus for literals. The completeness of the procedure is proved
using the the model generation technique, which allows us to justify
redundancy elimination based on appropriate orderings.
- Roberto Giacobazzi and Isabella Mastroeni
- Proving Abstract Non-Interference
- In this paper we introduce a compositional proof-system for certifying
abstract non-interference in programming languages. Certifying abstract
non-interference means proving that nounauthorized flow of information
is observable by the attacker from confidential to public data. The
properties of the computation that an attacker may observe are specified in
an abstract domain. Assertions specify the secrecy of a program relatively
to the given attacker and the proof-system specifies how these assertions
can be composed in a syntax-directed á la Hoare
deduction of secrecy.
We prove that the proof-system is sound relatively to the standard semantics
of an imperative programming language with non-deterministic choice. This
provides a sound proof-system for both certifying secrecy in language-based
security and deriving attackers which do not violate secrecy inductively
on program's syntax.
- Hugo Gimbert
- Parity and Exploration Games on Infinite Graphs
- This paper examines two players' turn-based perfect-information
games played on infinite graphs. Our attention is focused on the class of
games where winning conditions are boolean combinations of the following
two conditions: (1) the first one states that an infinite
play is won
by player 0 if during the play infinitely many different vertices were
visited, (2) the second one is the well known parity condition generalized
to a countable number of priorities. We show that, in most cases, both
players have positional winning strategies and we characterize their
respective winning sets. In the special case of pushdown graphs, we use
these results to show that the sets of winning positions are regular
and we show how to compute them as well as positional winning strategies
in exponential time.
- Jean Goubault-Larrecq, Slawomir
Lasota, David Nowak, and Yu Zhang
- Complete Lax Logical Relations for Cryptographic
Lambda-Calculi
- Security properties are usually expressed using notions of contextual
equivalence, to which logical relations are a powerful proof technique in
typed lambda calculi, e.g.,
Sumii and Pierce's logical relation for their
cryptographic lambda-calculus. We clarify Sumii and Pierce's approach,
using a cryptographic version of Moggi's monadic lambda-calculus as
framework, and show that their logical relations can be recovered by a
notion of lax logical relations. We also explore the question of fresh
names by using Stark's name creation monad and define logical relations
which are lax at encryption and function types but strict (non-lax)
at monad types. We show that they are sound and complete for contextual
equivalence at all types.
- Pierre Hyvernat
- Predicate Transformers and Linear Logic: yet another Denotational
Model
- In
the refinement calculus, monotonic predicate transformers are used to
model specifications for (imperative) programs. Together with a natural
notion of simulation, they form a category enjoying many algebraic
properties.
We build on this structure to make predicate transformers into a
denotational model of full linear logic: all the logical
constructions have a natural interpretation in terms of predicate
transformers (i.e., in terms of specifications). We then
interpret proofs of a formula by a safety property for the corresponding
specification.
- Neil Immerman, Alex Rabinovich, Tom Reps, Mooly
Sagiv, and Greta Yorsh
- The Boundary Between Decidability and Undecidability for Transitive
Closure Logics
-
To reason effectively about programs, it is important to have some
version of a transitive-closure operator so that we can describe such
notions as the set of nodes reachable from a program's variables. On
the other hand, with a few notable exceptions, adding transitive closure
to even very tame logics makes them undecidable. In this paper, we
explore the boundary between decidability and undecidability for
transitive-closure logics. Rabin proved that the monadic second-order
theory of trees is decidable, although the complexity of the decision
procedure is not elementary. If we go beyond trees, however,
undecidability comes immediately. We have identified a rather weak
language called EA(TC+[E]) that goes beyond trees, includes a version of
transitive closure, and is decidable. We show that satisfiability of
EA(TC+[E]) is NEXPTIME complete. We furthermore show that essentially
any reasonable extension of EA(TC+[E]) is undecidable. Our main
contribution is to demonstrate these sharp divisions between decidable
and undecidable. We also compare the complexity and expressibility of
EA(TC+[E]) with related decidable languages including MSO(trees) and
guarded fixed point logics. We mention possible applications to systems
some of us are building that use decidable logics to reason about
programs.
- Yukiyoshi Kameyama
- Axioms for Delimited Continuations in the CPS Hierarchy
-
A CPS translation is a syntactic translation of programs, which is
useful for describing their operational behavior. By iterating the
standard call-by-value CPS translation, Danvy and Filinski discovered
the CPS hierarchy and proposed a family of control operators, shift and
reset, that make it possible to capture successive delimited
continuations in a CPS hierarchy. Although shift and reset have found
their applications in several areas such as partial evaluation, most
studies in the literature have been devoted to the base level of the
hierarchy, namely, to level-1 shift and reset. In this article, we
investigate the whole family of shift and reset. We give a simple
calculus with level-n shift and level-n reset for an
arbitrary n>0. We
then give a set of equational axioms for them, and prove that these
axioms are sound and complete with respect to the CPS translation. The
resulting set of axioms is concise and a natural extension of those for
level-1 shift and reset.
- Margarita Korovina and Nicolai Vorobjov
- Pfaffian Hybrid Systems
-
It is well known that in an o-minimal hybrid system the continuous and
discrete components can be separated, and therefore the problem of
finite bisimulation reduces to the same problem for a transition system
associated with a continuous dynamical system. It was recently proved by
several authors that under certain natural assumptions such finite
bisimulation exists. In the paper we consider o-minimal systems defined
by Pfaffian functions, either implicitly (via triangular systems of
ordinary differential equations) or explicitly (by means of
semi-Pfaffian maps). We give explicit upper bounds on the sizes of
bisimulations as functions of formats of initial dynamical systems. We
also suggest an algorithm with an elementary (doubly-exponential) upper
complexity bound for computing finite bisimulations of these systems.
- Christopher Lynch
- Unsound Theorem Proving
-
We discuss the benefits of complete unsound inference procedures for
efficient methods of disproof. We give a framework for converting a
sound and complete saturation-based inference procedure into successive
unsound and complete procedures, that serve as successive approximations
to the theory. The idea is to successively add new statements in such a
way that the inference procedure will halt. Then the satisfiability is
evaluated over a stronger theory. This gives an over-approximation to
the given theory. We show how to successively compute better
over-approximations. Similarly, a sound and incomplete theorem prover
will give an under-approximation. In our framework, we successively
compute better over and under-approximations in this way. We illustrate
this framework with Knuth-Bendix Completion, and show that in some
theories this method becomes a decision procedure. Then we illustrate
the framework with a new method for the (nonground) word problem, based
on Congruence Closure. We show a class where this becomes a decision
procedure. Also, we show that this new inference system is interesting
in its own right. Given a particular goal, in many cases we can halt
the procedure at some point and say that all the equations for solving
the goal have been generated already. This is generally not possible in
Knuth-Bendix Completion.
- Patrick Maier
- Intuitionistic LTL and a New Characterization of Safety and
Liveness
- Classical linear-time temporal logic (LTL) is capable of specifying
of and reasoning about infinite behaviors only. While this is appropriate
for specifying non-terminating reactive systems, there are situations
(e.g., assume-guarantee reasoning, run-time verification) when it is
desirable to be able to reason about finite and infinite behaviors. We
propose an interpretation of the operators of LTL on finite and infinite
behaviors, which defines an intuitionistic temporal logic (ILTL).
We compare the expressive power of LTL and ILTL. We demonstrate that
ILTL is suitable for assume-guarantee reasoning and for expressing
properties that relate finite and infinite behaviors. In particular,
ILTL admits an elegant logical characterization of safety and liveness
properties.
- George Metcalfe, Nicola Olivetti,
and Dov Gabbay
- Goal-Directed Methods for Lukasiewicz Logic
- In this paper we present goal-directed deduction methods for
Lukasiewicz infinite-valued logic L, giving logic programming style
algorithms which both have a logical interpretation, and provide a
suitable basis for implementation. We begin by considering a basic version
with connections to calculi for other logics, then make refinements to
obtain greater efficiency and termination properties, and to treat further
connectives and truth constants. We finish by considering applications
of these algorithms to fuzzy logic programming.
- David Richerby
- Logical Characterizations of PSPACE
-
We present two, quite different, logical characterizations of the
computational complexity class PSPACE on unordered, finite relational
structures. The first of these, the closure of second-order logic under
the formation of partial fixed points is well-known in the folklore but
does not seem to be in the literature. The second, the closure of
first-order logic under taking partial fixed points and under an
operator for nondeterministic choice, is novel. We also present
syntactic normal forms for the two logics and compare the second with
other choice-based fixed-point logics found in the literature.
- Philipp Rohde
- Moving in a Crumbling Network: The Balanced Case
- In
this paper we continue the study of “sabotage modal logic” SML which
was suggested by van Benthem. In this logic one describes the
progression along edges of a transition graph in alternation with moves
of a saboteur who can delete edges. A drawback of the known results on
SML is the asymmetry of the two modalities of “moving” and
“deleting”.
Movements are local, whereas there is a global choice for edge deletion.
To balance the situation and to obtain a more realistic model for
traffic and network problems, we require that also the sabotage moves
(edge deletions) are subject to a locality condition. We show that the
new logic, called path sabotage logic PSL, already has the same
complexities as SML (model checking, satisfiability) and that it lacks
the finite model property. The main effort is finding a pruned form of
SML-models that can be enforced within PSL and giving appropriate
reductions from SML to PSL.
- Pawel Rychlikowski and Tomasz Truderung
- Set Constraints on Regular Terms
-
Set constraints are a useful formalism for verifying properties of
programs. Usually, they are interpreted over the universe of finite
terms. However, some logic languages allow infinite regular terms, so
it seems natural to consider set constraints over this domain. In the
paper we show that the satisfiability problem of set constraints over
regular terms is undecidable. We also show that, if each function symbol
has the arity at most 1, then this problem is EXPSPACE-complete.
- Ulrich Schöpp and Ian Stark
- A Dependent Type Theory with Names and Binding
- We consider the problem of providing formal support for working with
abstract syntax involving variable binders. Gabbay and Pitts have shown
in their work on Fraenkel-Mostowski (FM) set theory how to address this
through first-class names: in this paper we present a dependent type theory
for programming and reasoning with such names. Our development is based
on a categorical axiomatization of names, with freshness as its central
notion. An associated adjunction captures constructions known from FM
theory: the freshness quantifier, name-binding, and unique choice of
fresh names. We show that the Schanuel topos — the category underlying
FM set theory — is an instance of this axiomatization. Working from
the categorical structure, we define a dependent type theory which it
models. This uses bunches to integrate the monoidal structure corresponding
to freshness, from which we define novel multiplicative dependent products
and sums, as well as a propositions-as-types generalization of the freshness
quantifier.
- Lutz Schröder
- The Logic of the Partial λ-Calculus With Equality
- We investigate the logical aspects of the partial lambda-calculus with
equality, exploiting an equivalence between partial lambda-theories and
partial cartesian closed categories (pcccs) established here. The partial
lambda-calculus with equality provides a full-blown intuitionistic higher
order logic, which in a precise sense turns out to be almost the logic of
toposes, the distinctive feature of the latter being unique choice. We
prove in a linguistic fashion that the fundamental theorem of toposes
generalizes to pcccs with equality; type theoretically, this means that
the partial lambda-calculus with equality encompasses a Martin-Löf-style
dependent type theory. This work forms part of the semantical foundations
for the higher order algebraic specification language HasCASL.
- Aleksy Schubert
- On the Building of Affine Retractions
- A simple
type σ is retractable to a simple type τ if there are
two terms C:σ→τ and D:τ→σ
such that D°C = λx.x
w.r.t. βη-equivalence. The paper presents a system which
for given σ, τ derives affine retractability, i.e.,
the above relation with additional restriction that in C and
D every bound variable occurs at most once. A derivation in the
system constructs these terms. What is more, the complexity of building
affine retractions is studied. The problem of affine retractability is
NP-complete even for the class of types over single type atom and having
limited functional order. A polynomial algorithm for types of orders
less than 3 is also presented.
- Alan Skelley
- A Third-Order Bounded Arithmetic Theory for PSPACE
-
We present a novel third-order theory W11
of bounded arithmetic suitable for reasoning about PSPACE functions.
This theory has the advantages of avoiding the smash function symbol and
is otherwise much simpler than previous PSPACE theories. As an example
we outline a proof in W11
that from any configuration in the game of
Hex, at least one player has a winning strategy. We then exhibit a
translation of theorems of W11 into
families of propositional tautologies with polynomial-size proofs in
BPLK (a recent propositional proof system for PSPACE and an alternative
to G). This translation is clearer and more natural in several respects
than the analogous ones for previous PSPACE theories.
- Lutz Straßburger and
François Lamarche
- On Proof Nets for Multiplicative Linear Logic with Units
- In this paper we present a theory of proof nets for
multiplicative linear logic including the two units. It naturally
extends the well-known theory of unit-free multiplicative proof nets. A
linking is no longer a set of axiom links but a tree in which the axiom
links are subtrees. These trees will be identified according to an
equivalence relation based on a simple form of graph rewriting. We show
the standard results of sequentialization and strong normalization of
cut elimination. Furthermore, the identifications enforced on proofs
are such that the proof nets, as they are presented here, form the
arrows of the free (symmetric) *-autonomous category.
- Jérôme Vouillon
- Subtyping Union Types
- Subtyping
can be fairly complex for union types, due to interactions
with other types, such as function types. Furthermore,
these interactions turn out to depend on the calculus considered: for
instance, a call-by-value calculus and a call-by-name calculus will have
different possible subtyping rules. In order to abstract
ourselves away from this dependence, we consider a fairly large class of
calculi. This allows us to find a subtyping relation which is both
robust (it is sound for all calculi) and precise (it is complete with
respect to the class of calculi).
- Tjark Weber
- Towards Mechanized Program Verification with Separation
Logic
- Using separation logic, this paper presents three Hoare logics
(corresponding to different notions of correctness) for the simple While
language extended with commands for heap access and modification.
Properties of separating conjunction and separating implication
are mechanically verified and used to prove soundness and relative
completeness of all three Hoare logics. The whole development,
including a formal proof of the Frame Rule, is carried out in the
theorem prover Isabelle/HOL.
A BibTeX database is available as a separate
file.
An on-line
version of the conference
proceedings is available at Springer
www site.
Last modified:
Sep 14, 2004, 13:16