 |
 |
Special Issue for the Conference on Computer Science Logic (CSL) 2011
2011 Editors: Pawel Urzyczyn, Marc Bezem
1. Continuous Markovian Logics - Axiomatization and Quantified Metatheory
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".
2. L-Recursion and a new Logic for Logarithmic Space
We extend first-order logic with counting by a new operator that allows it to formalise a limited form of recursion which can be evaluated in logarithmic space. The resulting logic LREC has a data complexity in LOGSPACE, and it defines LOGSPACE-complete problems like deterministic reachability and Boolean formula evaluation. We prove that LREC is strictly more expressive than deterministic transitive closure logic with counting and incomparable in expressive power with symmetric transitive closure logic STC and transitive closure logic (with or without counting). LREC is strictly contained in fixed-point logic with counting FPC. We also study an extension LREC= of LREC that has nicer closure properties and is more expressive than both LREC and STC, but is still contained in FPC and has a data complexity in LOGSPACE. Our main results are that LREC captures LOGSPACE on the class of directed trees and that LREC= captures LOGSPACE on the class of interval graphs.
3. Non-idempotent intersection types and strong normalisation
We present a typing system with non-idempotent intersection types, typing a term syntax covering three different calculi: the pure {\lambda}-calculus, the calculus with explicit substitutions {\lambda}S, and the calculus with explicit substitutions, contractions and weakenings {\lambda}lxr. In each of the three calculi, a term is typable if and only if it is strongly normalising, as it is the case in (many) systems with idempotent intersections. Non-idempotency brings extra information into typing trees, such as simple bounds on the longest reduction sequence reducing a term to its normal form. Strong normalisation follows, without requiring reducibility techniques. Using this, we revisit models of the {\lambda}-calculus based on filters of intersection types, and extend them to {\lambda}S and {\lambda}lxr. Non-idempotency simplifies a methodology, based on such filter models, that produces modular proofs of strong normalisation for well-known typing systems (e.g. System F). We also present a filter model by means of orthogonality techniques, i.e. as an instance of an abstract notion of orthogonality model formalised in this paper and inspired by classical realisability. Compared to other instances based on terms (one of which rephrases a now standard proof of strong normalisation for the {\lambda}-calculus), the instance based on filters is shown to be better at proving strong normalisation results for {\lambda}S and {\lambda}lxr. Finally, the bounds on the longest reduction […]
4. Step-Indexed Relational Reasoning for Countable Nondeterminism
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for programming languages with countable nondeterminism is challenging. We present a step-indexed logical relations model of a higher-order functional programming language with countable nondeterminism and demonstrate how it can be used to reason about contextually defined may- and must-equivalence. In earlier step-indexed models, the indices have been drawn from {\omega}. Here the step-indexed relations for must-equivalence are indexed over an ordinal greater than {\omega}.
5. Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion
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.
6. Unifying Büchi Complementation Constructions
Complementation of Büchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kähler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a […]
7. Synthesis from Probabilistic Components
Synthesis is the automatic construction of a system from its specification. In classical synthesis algorithms, it is always assumed that the system is "constructed from scratch" rather than composed from reusable components. This, of course, rarely happens in real life, where almost every non-trivial commercial software system relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration, can be modeled as synthesis of a system from a library of components. Recently, Lustig and Vardi introduced dataflow and control-flow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while control-flow synthesis is decidable. In this work, we consider the problem of control-flow synthesis from libraries of probabilistic components . We show that this more general problem is also decidable.