ABSTRACT. We study foundational problems regarding the expressive power of parameterised systems. These (infinite-state) systems are composed of arbitrarily many finite-state processes that synchronise using a given communication primitive, i.e., broadcast, asynchronous rendezvous, broadcast with message loss, pairwise rendezvous, or disjunctive guards. With each communication primitive we associate the class of parameterised systems that use that primitive. We study the relative expressive power of these classes (can systems in one class be simulated by systems in another?) and provide a complete picture with only a single question left open. Motivated by the question of separating these classes, we also study the absolute expressive power (e.g., is the set of traces of every parameterised system of a given class omega-regular?). Our work gives insight into the verification and synthesis of parameterised systems, including new decidability and undecidability results of the model checking problem of parameterised systems using broadcast with message loss and asynchronous rendezvous.

ABSTRACT. Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment fLTL\GU, where U does not occur in the scope of G (but still F can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.

ABSTRACT. The implication problem for the class of embedded dependencies is undecidable. However, this does not imply lackness of a proof procedure as exemplified by the chase algorithm. In this paper we present a complete axiomatization of embedded dependencies that is based on the chase and uses inclusion dependencies and implicit existential quantification in the intermediate steps of deductions.

ABSTRACT. Graded path modalities count the number of paths satisfying a property, and generalize the existential (E) and universal (A) path modalities of CTL*. The resulting logic is denoted GCTL*, and is a very powerful logic since (as we show) it is equivalent, over trees, to monadic path logic. We settle the complexity of the satisfiability problem of GCTL*, i.e., TwoExpTime-Complete, and the complexity of the model checking problem of GCTL*, i.e., PSpace-Complete. The lower bounds already hold for CTL*, and so we supply the upper bounds. The significance of this work is two-fold: GCTL* is much more expressive than CTL* as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.

ABSTRACT. We define a call-by-value variant of Godel’s System T with references, and equip it with a linear dependent type and effect system, called dlT, that can estimate the complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, by showing that the type system over-approximates the complexity of executing programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of dlT. Finally, we demonstrate the usefulness of dlT for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.

ABSTRACT. The anti-subsumptive enforcement of a clause δ in a set of clauses ∆ consists in extracting one cardinality-maximal satisfiable subset ∆0 of ∆ ∪ {δ} that contains δ but that does not strictly subsume δ. In this paper, the computational issues of this problem are investigated in the Boolean framework. Especially, the minimal change policy that requires a minimal number of clauses to be dropped from ∆ can lead to an exponential computational blow-up. Indeed, a direct and natural approach to anti-subsumptive enforcement requires the computation of all inclusion-maximal subsets of ∆ ∪ {δ} that, at the same time, contain δ and are satisfiable with ¬δj where δj is some strict sub-clause of δ. On the contrary, we propose a method that avoids the computation of this possibly exponential number of subsets of clauses. Interestingly, it requires only one single call to a Partial-Max-SAT procedure and appears tractable in many realistic situations, even for very large ∆. Moreover, the approach is easily extended to take into account a preference pre-ordering between formulas and lay the foundations for the practical enumeration of all optimal solutions to the problem of making δ subsumption-free in ∆ under a minimal change policy.

ABSTRACT. We give a new proof of P-time completeness of the Linear Lambda Calculus, which was originally given by H. Mairson in 2003. Our proof uses an essentially different Boolean type from the type that Mairson used. Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.

ABSTRACT. Semantics-based applications encapsulate commonly a set of ontologies which represent knowledge formalized from different data sources. Some of these ontologies may change over time since, not only data would be updated but also our understanding on application domain would evolve. To ensure that ontologies remain usable, it is needed to revise ontologies in such a way that takes into account new knowledge and guarantees minimal changes. In this paper, we propose an ontology revision approach which allows one to use finite structures to characterize a set of models of an ontology, and to define a total pre-order over these structures. Thus, our revision operation satisfies all revision postulates. Moreover, we propose a procedure for revising an ontology expressed in an expressive description logic, namely SHIQ, and show that the resulting ontology remains expressible in SHIQ.

ABSTRACT. This paper discusses Ctrl, a tool to analyse – both automatically and manually – term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and can automatically verify termination, confluence and (to a limited extent) term equivalence using inductive theorem proving. Ctrl also offers a manual mode for inductive theorem proving, allowing support for and verification of "hand-written" term equivalence proofs.

ABSTRACT. Probabilistic coupling is a powerful tool for analyzing probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that characterizes both processes in the same probability space. Applications of coupling include reasoning about convergence of distributions, and stochastic dominance---a probabilistic version of a monotonicity property.

While the mathematical definition of coupling looks rather complex and difficult to manipulate, we show that the relational program logic pRHL---the logic underlying the EasyCrypt cryptographic proof assistant---internalizes a generalization of probabilistic coupling. We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verifying several couplings in EasyCrypt.

ABSTRACT. A good way to help users make decisions in an interactive application consists in suggesting choices in accordance with their preferences. This decision problem faces challenging tasks, mainly in choosing a good solution that satisfies users and reaches the defined goal. Classical decision methods take into account the goal, but not all the obtained decisions can satisfy users’ preferences. The originality of our explorative research is to associate Subjective Logic (SL) to system’s traces (historical information) in order to model the user preferences that improve the decision process. Following JØsang, SL provides a suitable framework for modeling and formally describing users’ preferences. We propose to connect data collected in past executions, called traces, to the user intuition in order to support subjective reasoning. Based on this result, we can choose a reasonable decision according to users’ preferences. A Tamagotchi system will be presented to validate our result.

ABSTRACT. We show how to implement a theorem prover for intuitionistic propositional logic, by combining a standard SAT-solver with a theory for intuitionistic implications. The result is a scalable theorem prover that also produces counter examples in the form of Kripke models.

ABSTRACT. One of the emergent trends in Proof Theory nowadays is the quest for proof search in modal logics. In fact, modalities are usually introduced via semantics and/or axioms, hence not lending to efficient implementations. The situation is slightly better for sequent calculi for modal logics. Unfortunately, the construction of suitable sequent calculi from semantic or axiomatic specifications is far from trivial. Moreover, even for some of the most basic modal logics, the currently known sequent calculi lack important properties such as cut elimination or a notion of normal proofs. A major obstacle to establishing these properties is the fact that such calculi usually do not exhibit distinct left and right introduction rules for the modalities. It turns out that this problem can be circumvent by using linear nested systems. The structures considered in this framework are linear sequences of ordinary sequents, and the rules for the modalities control the transfer of formulae from one sequent layer to another. In this work, we propose a general definition of labels for linear nested systems, giving rise to a focusing discipline for a class of modal systems. This opens the possibility of proposing automatic procedures for proof search in modal logics.

ABSTRACT. Preprocessing has been found vital for both search-based QBF solving with clause and cube learning (QCDCL) and solving by variable expansion. Among other QBF preprocessing techniques, blocked clause elimination (QBCE) simulates structural reasoning on formulas in prenex conjunctive normal form (PCNF) and reduces the bias introduced when translating non-PCNF formulas into PCNF. So far, the power of QBCE has not been exploited during solving.

We present the dynamic application of QBCE integrated in QCDCL solving. This dynamic application of QBCE is in sharp contrast to its typical use as a mere preprocessing technique. In our dynamic approach, QBCE is applied eagerly to the PCNF interpreted under the assignments that have currently been enumerated. The tight integration of QBCE in QCDCL results in a variant of cube learning which is exponentially stronger than traditional cube learning. We implemented our approach in the QBF solver DepQBF and ran experiments on instances from the QBF Gallery 2014. On application benchmarks, QCDCL with dynamic QBCE substantially outperforms traditional QCDCL. Moreover, our approach is compatible with incremental solving and can be combined with preprocessing techniques other than QBCE.

ABSTRACT. TIP is a toolbox for users and developers of inductive provers. It consists of a large number of tools which can, for example, simplify an inductive problem, monomorphise it or find counterexamples to it. We are using TIP to help maintain a set of benchmarks for inductive theorem provers, where its main job is to encode features that are not natively supported by the respective provers. TIP makes it easier to write inductive provers, by supplying necessary tools such as lemma discovery which prover authors can simply import into their own prover.