Model checking properties are often described by means of finite automata.
Any particular such automaton divides the set of infinite trees into finitely
many classes, according to which state has an infinite run. Building the full
type hierarchy upon this interpretation of the base type gives a finite
semantics for simply-typed lambda-trees.
A calculus based on this semantics is proven sound and complete. In
particular, for regular infinite lambda-trees it is decidable whether a given
automaton has a run or not. As regular lambda-trees are precisely recursion
schemes, this decidability result holds for arbitrary recursion schemes of
arbitrary level, without any syntactical restriction.
Two styles of definitions are usually considered to express that a security
protocol preserves the confidentiality of a data s. Reachability-based secrecy
means that s should never be disclosed while equivalence-based secrecy states
that two executions of a protocol with distinct instances for s should be
indistinguishable to an attacker. Although the second formulation ensures a
higher level of security and is closer to cryptographic notions of secrecy,
decidability results and automatic tools have mainly focused on the first
definition so far.
This paper initiates a systematic investigation of the situations where
syntactic secrecy entails strong secrecy. We show that in the passive case,
reachability-based secrecy actually implies equivalence-based secrecy for
digital signatures, symmetric and asymmetric encryption provided that the
primitives are probabilistic. For active adversaries, we provide sufficient
(and rather tight) conditions on the protocol for this implication to hold.
We study observation-based strategies for two-player turn-based games on
graphs with omega-regular objectives. An observation-based strategy relies on
imperfect information about the history of a play, namely, on the past sequence
of observations. Such games occur in the synthesis of a controller that does
not see the private state of the plant. Our main results are twofold. First, we
give a fixed-point algorithm for computing the set of states from which a
player can win with a deterministic observation-based strategy for any
omega-regular objective. The fixed point is computed in the lattice of
antichains of state sets. This algorithm has the advantages of being directed
by the objective and of avoiding an explicit subset construction on the game
graph. Second, we give an algorithm for computing the set of states from which
a player can win with probability 1 with a randomized observation-based
strategy for a Buechi objective. This set is of interest because in the absence
of perfect information, randomized strategies are more powerful than
deterministic ones. We show that our algorithms are optimal by proving matching
lower bounds.
For a two-variable formula ψ(X,Y) of Monadic Logic of Order (MLO) the
Church Synthesis Problem concerns the existence and construction of an operator
Y=F(X) such that ψ(X,F(X)) is universally valid over Nat.
Büchi and Landweber proved that the Church synthesis problem is
decidable; moreover, they showed that if there is an operator F that solves the
Church Synthesis Problem, then it can also be solved by an operator defined by
a finite state automaton or equivalently by an MLO formula. We investigate a
parameterized version of the Church synthesis problem. In this version ψ
might contain as a parameter a unary predicate P. We show that the Church
synthesis problem for P is computable if and only if the monadic theory of
<Nat,<,P> is decidable. We prove that the Büchi-Landweber theorem can be
extended only to ultimately periodic parameters. However, the MLO-definability
part of the Büchi-Landweber theorem holds for the parameterized version of
the Church synthesis problem.
In a previous work Baillot and Terui introduced Dual light affine logic
(DLAL) as a variant of Light linear logic suitable for guaranteeing complexity
properties on lambda calculus terms: all typable terms can be evaluated in
polynomial time by beta reduction and all Ptime functions can be represented.
In the present work we address the problem of typing lambda-terms in
second-order DLAL. For that we give a procedure which, starting with a term
typed in system F, determines whether it is typable in DLAL and outputs a
concrete typing if there exists any. We show that our procedure can be run in
time polynomial in the size of the original Church typed system F term.
ZF is a well investigated impredicative constructive version of
Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with
Replacement, which we call \izfr, along with its intensional counterpart
\iizfr. We define a typed lambda calculus $\li$ corresponding to proofs in
\iizfr according to the Curry-Howard isomorphism principle. Using realizability
for \iizfr, we show weak normalization of $\li$. We use normalization to prove
the disjunction, numerical existence and term existence properties. An inner
extensional model is used to show these properties, along with the set
existence property, for full, extensional \izfr.
Some type-based approaches to termination use sized types: an ordinal bound
for the size of a data structure is stored in its type. A recursive function
over a sized type is accepted if it is visible in the type system that
recursive calls occur just at a smaller size. This approach is only sound if
the type of the recursive function is admissible, i.e., depends on the size
index in a certain way. To explore the space of admissible functions in the
presence of higher-kinded data types and impredicative polymorphism, a
semantics is developed where sized types are interpreted as functions from
ordinals into sets of strongly normalizing terms. It is shown that upper
semi-continuity of such functions is a sufficient semantic criterion for
admissibility. To provide a syntactical criterion, a calculus for
semi-continuous functions is developed.
Forbidden Patterns Problems (FPPs) are a proper generalisation of Constraint
Satisfaction Problems (CSPs). However, we show that when the input is connected
and belongs to a class which has low tree-depth decomposition (e.g. structure
of bounded degree, proper minor closed class and more generally class of
bounded expansion) any FPP becomes a CSP. This result can also be rephrased in
terms of expressiveness of the logic MMSNP, introduced by Feder and Vardi in
relation with CSPs. Our proof generalises that of a recent paper by Nesetril
and Ossona de Mendez. Note that our result holds in the general setting of
problems over arbitrary relational structures (not just for graphs).
