We present the topos S of trees as a model of guarded recursion. We study the
internal dependently-typed higher-order logic of S and show that S models two
modal operators, on predicates and types, which serve as guards in recursive
definitions of terms, predicates, and types. In particular, we show how to
solve recursive type equations involving dependent types. We propose that the
internal logic of S provides the right setting for the synthetic construction
of abstract versions of step-indexed models of programming languages and
program logics. As an example, we show how to construct a model of a
programming language with higher-order store and recursive types entirely
inside the internal logic of S. Moreover, we give an axiomatic categorical
treatment of models of synthetic guarded domain theory and prove that, for any
complete Heyting algebra A with a well-founded basis, the topos of sheaves over
A forms a model of synthetic guarded domain theory, generalizing the results
for S.
The enriched effect calculus (EEC) is an extension of Moggi's computational
metalanguage with a selection of primitives from linear logic. This paper
explores the enriched effect calculus as a target language for
continuation-passing-style (CPS) translations in which the typing of the
translations enforces the linear usage of continuations. We first observe that
established call-by-value and call-by name linear-use CPS translations of
simply-typed lambda-calculus into intuitionistic linear logic (ILL) land in the
fragment of ILL given by EEC. These two translations are uniformly generalised
by a single generic translation of the enriched effect calculus into itself. As
our main theorem, we prove that the generic self-translation of EEC is
involutive up to isomorphism. As corollaries, we obtain full completeness
results, both for the generic translation, and for the original call-by-value
and call-by-name translations.
We study the semantics of a resource-sensitive extension of the lambda
calculus in a canonical reflexive object of a category of sets and relations, a
relational version of Scott's original model of the pure lambda calculus. This
calculus is related to Boudol's resource calculus and is derived from Ehrhard
and Regnier's differential extension of Linear Logic and of the lambda
calculus. We extend it with new constructions, to be understood as implementing
a very simple exception mechanism, and with a "must" parallel composition.
These new operations allow to associate a context of this calculus with any
point of the model and to prove full abstraction for the finite sub-calculus
where ordinary lambda calculus application is not allowed. The result is then
extended to the full calculus by means of a Taylor Expansion formula. As an
intermediate result we prove that the exception mechanism is not essential in
the finite sub-calculus.
Mixing induction and coinduction, we study alternative definitions of streams
being finitely red. We organize our definitions into a hierarchy including also
some well-known alternatives in intuitionistic analysis. The hierarchy
collapses classically, but is intuitionistically of strictly decreasing
strength. We characterize the differences in strength in a precise way by weak
instances of the Law of Excluded Middle.
Let \Gamma be a structure with a finite relational signature and a
first-order definition in (R;*,+) with parameters from R, that is, a relational
structure over the real numbers where all relations are semi-algebraic sets. In
this article, we study the computational complexity of constraint satisfaction
problem (CSP) for \Gamma: the problem to decide whether a given primitive
positive sentence is true in \Gamma. We focus on those structures \Gamma that
contain the relations \leq, {(x,y,z) | x+y=z} and {1}. Hence, all CSPs studied
in this article are at least as expressive as the feasibility problem for
linear programs. The central concept in our investigation is essential
convexity: a relation S is essentially convex if for all a,b\inS, there are
only finitely many points on the line segment between a and b that are not in
S. If \Gamma contains a relation S that is not essentially convex and this is
witnessed by rational points a,b, then we show that the CSP for \Gamma is
NP-hard. Furthermore, we characterize essentially convex relations in logical
terms. This different view may open up new ways for identifying tractable
classes of semi-algebraic CSPs. For instance, we show that if \Gamma is a
first-order expansion of (R;*,+), then the CSP for \Gamma can be solved in
polynomial time if and only if all relations in \Gamma are essentially convex
(unless P=NP).
For many application-level distributed protocols and parallel algorithms, the
set of participants, the number of messages or the interaction structure are
only known at run-time. This paper proposes a dependent type theory for
multiparty sessions which can statically guarantee type-safe, deadlock-free
multiparty interactions among processes whose specifications are parameterised
by indices. We use the primitive recursion operator from Gödel's System T to
express a wide range of communication patterns while keeping type checking
decidable. To type individual distributed processes, a parameterised global
type is projected onto a generic generator which represents a class of all
possible end-point types. We prove the termination of the type-checking
algorithm in the full system with both multiparty session types and recursive
types. We illustrate our type theory through non-trivial programming and
verification examples taken from parallel algorithms and Web services usecases.
PCF is a sequential simply typed lambda calculus language. There is a unique
order-extensional fully abstract cpo model of PCF, built up from equivalence
classes of terms. In 1979, Gérard Berry defined the stable order in this
model and proved that the extensional and the stable order together form a
bicpo. He made the following two conjectures: 1) "Extensional and stable order
form not only a bicpo, but a bidomain." We refute this conjecture by showing
that the stable order is not bounded complete, already for finitary PCF of
second-order types. 2) "The stable order of the model has the syntactic order
as its image: If a is less than b in the stable order of the model, for finite
a and b, then there are normal form terms A and B with the semantics a, resp.
b, such that A is less than B in the syntactic order." We give counter-examples
to this conjecture, again in finitary PCF of second-order types, and also
refute an improved conjecture: There seems to be no simple syntactic
characterization of the stable order. But we show that Berry's conjecture is
true for unary PCF. For the preliminaries, we explain the basic fully abstract
semantics of PCF in the general setting of (not-necessarily complete) partial
order models (f-models.) And we restrict the syntax to "game terms", with a
graphical representation.
This article proposes novel off-line test generation techniques from
non-deterministic timed automata with inputs and outputs (TAIOs) in the formal
framework of the tioco conformance theory. In this context, a fi?rst problem is
the determinization of TAIOs, which is necessary to foresee next enabled
actions after an observable trace, but is in general impossible because not all
timed automata are determinizable. This problem is solved thanks to an
approximate determinization using a game approach. The algorithm performs an
io-abstraction which preserves the tioco conformance relation and thus
guarantees the soundness of generated test cases. A second problem is the
selection of test cases from a TAIO speci?fication. The selection here relies
on a precise description of timed behaviors to be tested which is carried out
by expressive test purposes modeled by a generalization of TAIOs. Finally, an
algorithm is described which generates test cases in the form of TAIOs equipped
with verdicts, using a symbolic co-reachability analysis guided by the test
purpose. Properties of test cases are then analyzed with respect to the
precision of the approximate determinization: when determinization is exact,
which is the case on known determinizable classes, in addition to soundness,
properties characterizing the adequacy of test cases verdicts are also
guaranteed.
We investigate the decidability and complexity status of model-checking
problems on unlabelled reachability graphs of Petri nets by considering
first-order and modal languages without labels on transitions or atomic
propositions on markings. We consider several parameters to separate decidable
problems from undecidable ones. Not only are we able to provide precise borders
and a systematic analysis, but we also demonstrate the robustness of our proof
techniques.
Path checking, the special case of the model checking problem where the model
under consideration is a single path, plays an important role in monitoring,
testing, and verification. We prove that for linear-time temporal logic (LTL),
path checking can be efficiently parallelized. In addition to the core logic,
we consider the extensions of LTL with bounded-future (BLTL) and past-time
(LTL+Past) operators. Even though both extensions improve the succinctness of
the logic exponentially, path checking remains efficiently parallelizable: Our
algorithm for LTL, LTL+Past, and BLTL+Past is in AC^1(logDCFL) \subseteq NC.
A system of linear dependent types for the lambda calculus with full
higher-order recursion, called dlPCF, is introduced and proved sound and
relatively complete. Completeness holds in a strong sense: dlPCF is not only
able to precisely capture the functional behaviour of PCF programs (i.e. how
the output relates to the input) but also some of their intensional properties,
namely the complexity of evaluating them with Krivine's Machine. dlPCF is
designed around dependent types and linear logic and is parametrized on the
underlying language of index terms, which can be tuned so as to sacrifice
completeness for tractability.
We consider a specific class of tree structures that can represent basic
structures in linguistics and computer science such as XML documents, parse
trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We
present axiomatizations of the monadic second-order logic (MSO), monadic
transitive closure logic (FO(TC1)) and monadic least fixed-point logic
(FO(LFP1)) theories of this class of structures. These logics can express
important properties such as reachability. Using model-theoretic techniques, we
show by a uniform argument that these axiomatizations are complete, i.e., each
formula that is valid on all finite trees is provable using our axioms. As a
backdrop to our positive results, on arbitrary structures, the logics that we
study are known to be non-recursively axiomatizable.
We propose the concept of adaptable processes as a way of overcoming the
limitations that process calculi have for describing patterns of dynamic
process evolution. Such patterns rely on direct ways of controlling the
behavior and location of running processes, and so they are at the heart of the
adaptation capabilities present in many modern concurrent systems. Adaptable
processes have a location and are sensible to actions of dynamic update at
runtime; this allows to express a wide range of evolvability patterns for
concurrent processes. We introduce a core calculus of adaptable processes and
propose two verification problems for them: bounded and eventual adaptation.
While the former ensures that the number of consecutive erroneous states that
can be traversed during a computation is bound by some given number k, the
latter ensures that if the system enters into a state with errors then a state
without errors will be eventually reached. We study the (un)decidability of
these two problems in several variants of the calculus, which result from
considering dynamic and static topologies of adaptable processes as well as
different evolvability patterns. Rather than a specification language, our
calculus intends to be a basis for investigating the fundamental properties of
evolvable processes and for developing richer languages with evolvability
capabilities.
We present a both simple and comprehensive graphical calculus for quantum
computing. In particular, we axiomatize the notion of an environment, which
together with the earlier introduced axiomatic notion of classical structure
enables us to define classical channels, quantum measurements and classical
control. If we moreover adjoin the earlier introduced axiomatic notion of
complementarity, we obtain sufficient structural power for constructive
representation and correctness derivation of typical quantum informatic
protocols.
The biggest challenge in hybrid systems verification is the handling of
differential equations. Because computable closed-form solutions only exist for
very simple differential equations, proof certificates have been proposed for
more scalable verification. Search procedures for these proof certificates are
still rather ad-hoc, though, because the problem structure is only understood
poorly. We investigate differential invariants, which define an induction
principle for differential equations and which can be checked for invariance
along a differential equation just by using their differential structure,
without having to solve them. We study the structural properties of
differential invariants. To analyze trade-offs for proof search complexity, we
identify more than a dozen relations between several classes of differential
invariants and compare their deductive power. As our main results, we analyze
the deductive power of differential cuts and the deductive power of
differential invariants with auxiliary differential variables. We refute the
differential cut elimination hypothesis and show that, unlike standard cuts,
differential cuts are fundamental proof principles that strictly increase the
deductive power. We also prove that the deductive power increases further when
adding auxiliary differential variables to the dynamics.
We address a fundamental mismatch between the combinations of dynamics that
occur in cyber-physical systems and the limited kinds of dynamics supported in
analysis. Modern applications combine communication, computation, and control.
They may even form dynamic distributed networks, where neither structure nor
dimension stay the same while the system follows hybrid dynamics, i.e., mixed
discrete and continuous dynamics. We provide the logical foundations for
closing this analytic gap. We develop a formal model for distributed hybrid
systems. It combines quantified differential equations with quantified
assignments and dynamic dimensionality-changes. We introduce a dynamic logic
for verifying distributed hybrid systems and present a proof calculus for this
logic. This is the first formal verification approach for distributed hybrid
systems. We prove that our calculus is a sound and complete axiomatization of
the behavior of distributed hybrid systems relative to quantified differential
equations. In our calculus we have proven collision freedom in distributed car
control even when an unbounded number of new cars may appear dynamically on the
road.
The probabilistic modal {\mu}-calculus is a fixed-point logic designed for
expressing properties of probabilistic labeled transition systems (PLTS's). Two
equivalent semantics have been studied for this logic, both assigning to each
state a value in the interval [0,1] representing the probability that the
property expressed by the formula holds at the state. One semantics is
denotational and the other is a game semantics, specified in terms of
two-player stochastic parity games. A shortcoming of the probabilistic modal
{\mu}-calculus is the lack of expressiveness required to encode other important
temporal logics for PLTS's such as Probabilistic Computation Tree Logic (PCTL).
To address this limitation we extend the logic with a new pair of operators:
independent product and coproduct. The resulting logic, called probabilistic
modal {\mu}-calculus with independent product, can encode many properties of
interest and subsumes the qualitative fragment of PCTL. The main contribution
of this paper is the definition of an appropriate game semantics for this
extended probabilistic {\mu}-calculus. This relies on the definition of a new
class of games which generalize standard two-player stochastic (parity) games
by allowing a play to be split into concurrent subplays, each continuing their
evolution independently. Our main technical result is the equivalence of the
two semantics. The proof is carried out in ZFC set theory extended with
Martin's Axiom at an uncountable cardinal.
Continuous Markovian Logic (CML) is a multimodal logic that expresses
quantitative and qualitative properties of continuous-time labelled Markov
processes with arbitrary (analytic) state-spaces, henceforth called continuous
Markov processes (CMPs). The modalities of CML evaluate the rates of the
exponentially distributed random variables that characterize the duration of
the labeled transitions of a CMP. In this paper we present weak and strong
complete axiomatizations for CML and prove a series of metaproperties,
including the finite model property and the construction of canonical models.
CML characterizes stochastic bisimilarity and it supports the definition of a
quantified extension of the satisfiability relation that measures the
"compatibility" between a model and a property. In this context, the
metaproperties allows us to prove two robustness theorems for the logic stating
that one can perturb formulas and maintain "approximate satisfaction".
