Foundations of Software Science and Computation Structures

Frontmatter

PDF

Open Access

Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata

Abstract

We explore the suitability of mod 2 multiplicity automata (M2MAs) as a representation for regular languages of infinite words. M2MAs are a deterministic representation that is known to be learnable in polynomial time with membership and equivalence queries, in contrast to many other representations. Another advantage of M2MAs compared to non-deterministic automata is that their equivalence can be decided in polynomial time and complementation incurs only an additive constant size increase. Because learning time is parameterized by the size of the representation, particular attention is focused on the relative succinctness of alternate representations, in particular, LTL formulas and Büchi automata of the types: deterministic, non-deterministic and strongly unambiguous. We supplement the theoretical results of worst case upper and lower bounds with experimental results computed for randomly generated automata and specific families of LTL formulas.

Dana Angluin, Timos Antonopoulos, Dana Fisman, Nevin George

PDF

Open Access

Limits and difficulties in the design of under-approximation abstract domains

Abstract

Static analyses are mostly designed to show the absence of bugs: if the analysis reports no alarms then the program won’t exhibit any unwanted behaviours. To this aim they manipulate over-approximations of program semantics and, inevitably, they often report some false alarms. Recently, O’Hearn proposed Incorrectness Logic, that is based on under-approximations, as a formal method to find bugs that only reports true alarms. In this paper we aim to answer one important question raised by O’Hearn, namely which role can Abstract Interpretation play for the development of under-approximate tools for bug catching. In principle, Abstract Interpretation based static analyses can be defined for computing over-approximations as well as under-approximations, but in practice, most techniques exploited the former while few attempts developed the latter. To show why it is difficult to design effective under-approximation abstract domains, we first propose the new definitions of non emptying functions and highly surjective function family and then we formally prove the limits of under-approximation analysis by showing the non existence of abstract domains able to approximate such functions in a non trivial way. Our results outline the limits of under-approximation Abstract Interpretation and clarify, for the first time, why over- and under- approximation analyzers exhibited such a different development.

Flavio Ascari, Roberto Bruni, Roberta Gori

PDF

Open Access

On probability-raising causality in Markov decision processes

Abstract

The purpose of this paper is to introduce a notion of causality in Markov decision processes based on the probability-raising principle and to analyze its algorithmic properties. The latter includes algorithms for checking cause-effect relationships and the existence of probability-raising causes for given effect scenarios. Inspired by concepts of statistical analysis, we study quality measures (recall, coverage ratio and f-score) for causes and develop algorithms for their computation. Finally, the computational complexity for finding optimal causes with respect to these measures is analyzed.

Christel Baier, Florian Funke, Jakob Piribauer, Robin Ziemek

PDF

Open Access

Parameterized Analysis of Reconfigurable Broadcast Networks

Abstract

Reconfigurable broadcast networks (RBN) are a model of distributed computation in which agents can broadcast messages to other agents using some underlying communication topology which can change arbitrarily over the course of executions. In this paper, we conduct parameterized analysis of RBN. We consider cubes, (infinite) sets of configurations in the form of lower and upper bounds on the number of agents in each state, and we show that we can evaluate boolean combinations over cubes and reachability sets of cubes in PSPACE. In particular, reachability from a cube to another cube is a PSPACE-complete problem.

To prove the upper bound for this parameterized analysis, we prove some structural properties about the reachability sets and the symbolic graph abstraction of RBN, which might be of independent interest. We justify this claim by providing two applications of these results. First, we show that the almost-sure coverability problem is PSPACE-complete for RBN, thereby closing a complexity gap from a previous paper [3]. Second, we define a computation model using RBN, à la population protocols, called RBN protocols. We characterize precisely the set of predicates that can be computed by such protocols.

A. R. Balasubramanian, Lucie Guillou, Chana Weil-Kennedy

PDF

Open Access

Separators in Continuous Petri Nets

Abstract

Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking \(\boldsymbol{m}_\text {src}\) cannot reach a marking \(\boldsymbol{m}_\text {tgt}\), then there is a formula \(\varphi \) of Presburger arithmetic such that: \(\varphi (\boldsymbol{m}_\text {src})\) holds; \(\varphi \) is forward invariant, i.e., \(\varphi (\boldsymbol{m})\) and \(\boldsymbol{m} \rightarrow \boldsymbol{m}'\) imply \(\varphi (\boldsymbol{m}'\)); and \(\lnot \varphi (\boldsymbol{m}_\text {tgt})\) holds. While these separators could be used as explanations and as formal certificates of unreachability, this has not yet been the case due to their (super-)Ackermannian worst-case size and the (super-)exponential complexity of checking that a formula is a separator. We show that, in continuous Petri nets, these two problems can be overcome. We introduce locally closed separators, and prove that: (a) unreachability can be witnessed by a locally closed separator computable in polynomial time; (b) checking whether a formula is a locally closed separator is in NC (so, simpler than unreachablity, which is P-complete).

Michael Blondin, Javier Esparza

PDF

Open Access

Graphical Piecewise-Linear Algebra

Abstract

Graphical (Linear) Algebra is a family of diagrammatic languages allowing to reason about different kinds of subsets of vector spaces compositionally. It has been used to model various application domains, from signal-flow graphs to Petri nets and electrical circuits. In this paper, we introduce to the family its most expressive member to date: Graphical Piecewise-Linear Algebra, a new language to specify piecewise-linear subsets of vector spaces.

Like the previous members of the family, it comes with a complete axiomatisation, which means it can be used to reason about the corresponding semantic domain purely equationally, forgetting the set-theoretic interpretation. We show completeness using a single axiom on top of Graphical Polyhedral Algebra, and show that this extension is the smallest that can capture a variety of relevant constructs.

Finally, we showcase its use by modelling the behaviour of stateless electronic circuits of ideal elements, a domain that had remained outside the remit of previous diagrammatic languages.

Guillaume Boisseau, Robin Piedeleu

PDF

Open Access

Token Games and History-Deterministic Quantitative Automata

Abstract

A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given nondeterministic automaton is history-deterministic (the HDness problem) is generally a difficult task, which might involve an exponential procedure, or even be undecidable, for example for pushdown automata. Token games provide a PTime solution to the HDness problem of Büchi and coBüchi automata, and it is conjectured that 2-token games characterise HDness for all \(\omega \)-regular automata. We extend token games to the quantitative setting and analyze their potential to help deciding HDness for quantitative automata. In particular, we show that 1-token games characterise HDness for all quantitative (and Boolean) automata on finite words, as well as discounted-sum (\({\mathsf {DSum}}\)) automata on infinite words, and that 2-token games characterise HDness of \({\mathsf {LimInf}}\) and \({\mathsf {LimSup}}\) automata. Using these characterisations, we provide solutions to the HDness problem of \({\mathsf {Inf}}\) and \({\mathsf {Sup}}\) automata on finite words in PTime, for \({\mathsf {DSum}}\) automata on finite and infinite words in NP\(\cap \) co-NP, for \({\mathsf {LimSup}}\) automata in quasipolynomial time, and for \({\mathsf {LimInf}}\) automata in exponential time, where the latter two are only polynomial for automata with a logarithmic number of weights.

Udi Boker, Karoliina Lehtinen

PDF

Open Access

On the Translation of Automata to Linear Temporal Logic

Abstract

While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic \(\omega \)-regular automata to LTL.

Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consists of a translation of general counter-free deterministic \(\omega \)-regular automata into LTL formulas of double exponential temporal-nesting depth and triple exponential length, using an intermediate Krohn-Rhodes cascade decomposition of the automaton. To our knowledge, this is the first elementary bound on this translation. Furthermore, our translation preserves the acceptance condition of the automaton in the sense that it turns a looping, weak, Büchi, coBüchi or Muller automaton into a formula that belongs to the matching class of the syntactic future hierarchy. In particular, it can be used to translate an LTL formula recognising a safety language to a formula belonging to the safety fragment of LTL (over both finite and infinite words).

Udi Boker, Karoliina Lehtinen, Salomon Sickert

PDF

Open Access

Categorical composable cryptography

Abstract

We formalize the simulation paradigm of cryptography in terms of category theory and show that protocols secure against abstract attacks form a symmetric monoidal category, thus giving an abstract model of composable security definitions in cryptography. Our model is able to incorporate computational security, set-up assumptions and various attack models such as colluding or independently acting subsets of adversaries in a modular, flexible fashion. We conclude by using string diagrams to rederive the security of the one-time pad and no-go results concerning the limits of bipartite and tripartite cryptography, ruling out e.g., composable commitments and broadcasting.

Anne Broadbent, Martti Karvonen

PDF

Open Access

DyNetKAT: An Algebra of Dynamic Networks

Abstract

We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT – a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.

Georgiana Caltais, Hossein Hojjat, Mohammad Reza Mousavi, Hünkar Can Tunç

PDF

Open Access

A new criterion for -adhesivity, with an application to hierarchical graphs

Abstract

Adhesive categories provide an abstract framework for the algebraic approach to rewriting theory, where many general results can be recast and uniformly proved. However, checking that a model satisfies the adhesivity properties is sometimes far from immediate. In this paper we present a new criterion giving a sufficient condition for \(\mathcal {M},\mathcal {N}\)-adhesivity, a generalisation of the original notion of adhesivity. We apply it to several existing categories, and in particular to hierarchical graphs, a formalism that is notoriously difficult to fit in the mould of algebraic approaches to rewriting and for which various alternative definitions float around.

Davide Castelnovo, Fabio Gadducci, Marino Miculan

PDF

Open Access

Quantifier elimination for counting extensions of Presburger arithmetic

Abstract

We give a new quantifier elimination procedure for Presburger arithmetic extended with a unary counting quantifier \(\exists ^{= x} y\, \mathrm {\Phi }\) that binds to the variable \(x\) the number of different \(y\) satisfying \(\mathrm {\Phi }\). While our procedure runs in non-elementary time in general, we show that it yields nearly optimal elementary complexity results for expressive counting extensions of Presburger arithmetic, such as the threshold counting quantifier \(\exists ^{\ge c} y\, \mathrm {\Phi }\) that requires that the number of different y satisfying \(\mathrm {\Phi }\) be at least \(c\in \mathbb {N}\), where c can succinctly be defined by a Presburger formula. Our results are cast in terms of what we call the monadically-guarded fragment of Presburger arithmetic with unary counting quantifiers, for which we develop a 2ExpSpace decision procedure.

Dmitry Chistikov, Christoph Haase, Alessio Mansutti

PDF

Open Access

A first-order logic characterisation of safety and co-safety languages

Abstract

Linear Temporal Logic (\(\mathsf {LTL}\)) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Its widespread use is also due to its strong foundational properties. One of them is Kamp’s theorem, showing that \(\mathsf {LTL}\) and the first-order theory of one successor (\(\mathsf {S1S}[\mathsf {FO}]\)) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for \(\mathsf {LTL}\). \(\mathsf {Safety\text {-} \mathsf {LTL}}\) (resp., \(\mathsf {coSafety\text {-} \mathsf {LTL}}\)) is a fragment of \(\mathsf {LTL}\) where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of \(\mathsf {S1S}[\mathsf {FO}]\), called \(\mathsf {Safety\text {-} FO}\), and its dual \(\mathsf {coSafety\text {-} FO}\), which are expressively complete with regards to the \(\mathsf {LTL}\)-definable safety languages. In particular, we prove that they respectively characterise exactly \(\mathsf {Safety\text {-} \mathsf {LTL}}\) and \(\mathsf {coSafety\text {-} \mathsf {LTL}}\), a result that joins Kamp’s theorem, and provides a clearer view of the charactisations of (fragments of) \(\mathsf {LTL}\) in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in \(\mathsf {LTL}\) is definable in \(\mathsf {Safety\text {-} \mathsf {LTL}}\) as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of \(\mathsf {Safety\text {-} \mathsf {LTL}}\) interpreted over finite and infinite traces.

Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta

PDF

Open Access

First-order separation over countable ordinals

Abstract

We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on \(\omega \)-words. For this, we develop the algebraic concept of monoid (resp. \(\omega \)-semigroup, resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp. \(\omega \)-semigroup, resp. ordinal monoid) that explicitly includes a new operation capturing the loss of precision induced by first-order indistinguishability. We also show the computability of FO-pointlike sets, and the decidability of the covering problem for first-order logic on countable ordinal words.

Thomas Colcombet, Sam van Gool, Rémi Morvan

PDF

Open Access

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications

Abstract

We introduce a call-by-name lambda-calculus \(\lambda J\) with generalized applications which integrates a notion of distant reduction that allows to unblock \(\beta \)-redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization –that we relate to others in the literature–, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus \(\lambda J\) and the well-know calculus \(\varLambda J\) determine equivalent notions of strong normalization. As a consequence, \(\varLambda J\) inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for \(\lambda J\), despite the fact that quantitative subject reduction fails for permutative conversions.

José Espírito Santo, Delia Kesner, Loïc Peyrot

PDF

Open Access

Modal Logics and Local Quantifiers: A Zoo in the Elementary Hierarchy

Abstract

We study a family of modal logics interpreted on tree-like structures, and featuring local quantifiers \(\exists ^{k}p\) that bind the proposition p to worlds that are accessible from the current one in at most k steps. We consider a first-order and a second-order semantics for the quantifiers, which enables us to relate several well-known formalisms, such as hybrid logics, \(\textsf {S5Q}\) and graded modal logic. To better stress these connections, we explore fragments of our logics, called herein round-bounded fragments. Depending on whether first or second-order semantics is considered, these fragments populate the hierarchy \({2\textsc {NExp} \subset 3\textsc {NExp} \subset \cdots }\) or the hierarchy \({2\textsc {AExp}_{pol} \subset 3\textsc {AExp}_{pol} \subset \cdots }\), respectively. For formulae up-to modal depth k, the complexity improves by one exponential.

Raul Fervari, Alessio Mansutti

PDF

Open Access

Temporal Stream Logic modulo Theories

Abstract

Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive enough. In the semantics of TSL, functions and predicates are left uninterpreted. In this paper, we extend TSL with first-order theories, enabling us to specify systems using interpreted functions and predicates such as incrementation or equality. We investigate the satisfiability problem of TSL modulo the standard underlying theory of uninterpreted functions as well as with respect to Presburger arithmetic and the theory of equality: For all three theories, TSL satisfiability is neither semi-decidable nor co-semi-decidable. Nevertheless, we identify three fragments of TSL for which the satisfiability problem is (semi-)decidable in the theory of uninterpreted functions. Despite the undecidability, we present an algorithm – which is not guaranteed to terminate – for checking the satisfiability of a TSL formula in the theory of uninterpreted functions and evaluate it: It scales well and is able to validate assumptions in a real-world system design.

Bernd Finkbeiner, Philippe Heim, Noemi Passing

PDF

Open Access

The Different Shades of Infinite Session Types

Abstract

Many type systems include infinite types. In session type systems, infinite types are important because they specify communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions or by non-parametric equational definitions . Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through various forms of parametric equational definitions, to arbitrary infinite types in a coinductively defined space. We study infinite session types across a spectrum of shades of grey on the way to the bright light of general infinite types. We identify four points on the spectrum, characterised by different styles of equational definitions, and show that they form a strict hierarchy by establishing bidirectional correspondences with classes of automata: finite-state, 1-counter, pushdown and 2-counter. This allows us to establish decidability and undecidability results for type formation, type equivalence and duality in each class of types. We also consider previous work on context-free session types (and extend it to higher-order) and nested session types, and locate them on our spectrum of infinite types.

Simon J. Gay, Diogo Poças, Vasco T. Vasconcelos

PDF

Open Access

Complete and tractable machine-independent characterizations of second-order polytime

Abstract

The class of Basic Feasible Functionals \(\mathtt{BFF}\) is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of \(\mathtt{BFF}\) based on a typed programming language of terms. These terms may perform calls to imperative procedures, which are not recursive. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. \(\mathtt{BFF}\) consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of \(\mathtt{BFF}\), thus solving a problem opened for more than 20 years.

Emmanuel Hainry, Bruce M. Kapron, Jean-Yves Marion, Romain Péchoux

PDF

Open Access

Variable binding and substitution for (nameless) dummies

Abstract

By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi

PDF

Open Access

Uniform Guarded Fragments

Abstract

In this paper we prove that the uniform one-dimensional guarded fragment, which is a natural polyadic generalization of guarded two-variable logic, has the Craig interpolation property. We will also prove that the satisfiability problem of uniform guarded fragment is NExpTime-complete.

Reijo Jaakkola

PDF

Open Access

Sweedler Theory of Monads

Abstract

Monad-comonad interaction laws are a mathematical concept for describing communication protocols between effectful computations and coeffectful environments in the paradigm where notions of effectful computation are modelled by monads and notions of coeffectful environment by comonads. We show that monad-comonad interaction laws are an instance of measuring maps from Sweedler theory for duoidal categories whereby the final interacting comonad for a monad and a residual monad arises as the Sweedler hom and the initial residual monad for a monad and an interacting comonad as the Sweedler copower. We then combine this with a (co)algebraic characterization of monad-comonad interaction laws to derive descriptions of the Sweedler hom and the Sweedler copower in terms of their coalgebras resp. algebras.

Dylan McDermott, Exequiel Rivas, Tarmo Uustalu

PDF

Open Access

Model Checking Temporal Properties of Recursive Probabilistic Programs

Abstract

Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on \(\omega \)-regular and LTL properties. In this paper, we study the model checking problem of pPDA against \(\omega \)-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than \(\omega \)-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.

Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen

PDF

Backmatter

PDF