ABSTRACT. We propose an algebraic approach to stochastic graph-rewriting which extends the classical construction of the Heisenberg-Weyl algebra and its canonical representation on the Fock space. Rules are seen as particular elements of an algebra of `diagrams' (the diagram algebra $\mathscr{D}$). Diagrams can be thought of as formal computational traces represented in partial time. They span a vector space which carries a natural filtered Hopf algebra structure. Diagrams can be evaluated to normal diagrams (each corresponding to a rule) and generate an associative unital (non-commutative) $\ast$-algebra of rules (the rule algebra $\mathscr{R}$). Evaluation becomes a morphism of unital associative algebras which maps general diagrams in $\mathscr{D}$ to normal ones in $\mathscr{R}$. In this algebraic reformulation, usual distinctions between graph observables (real-valued maps on the set of graphs defined by counting subgraphs), and rules disappear. Instead, natural algebraic substructures of $\mathscr{R}$ arise: formal observables are seen as rules with equal left and right hand sides and form a commutative subalgebra, the ones counting subgraphs forming a sub-subalgebra of identity rules. Actual graph-rewriting (of the DPO type) is recovered as a canonical \emph{representation} of the rule algebra as linear operators over the vector field generated by (isomorphism classes of) finite graphs. The construction of the representation is in close analogy and subsumes the classical (multi-type bosonic) Fock space representation of the Heisenberg-Weyl algebra.

This subtle shift of point of view (away from its canonical representation to the rule algebra itself) has far-reaching and unexpected consequences. We find that natural variants of the evaluation morphism map give rise to concepts of graph transformations hitherto not considered (these will be described in a separate paper, as in this extended abstract we limit ourselves to the simplest concept namely that of DPO-rewriting). We prove very simply a DPO version of the jump-closure theorem, namely that the sub-space of representations of formal graph observables closed under the action of any rule set. From this new jump-closure result follows that for any set of rules $\mathcal{R}$, one can derive a formal and self-consistent Kolmogorov backward equation for (representations) of formal observables.

ABSTRACT. This paper shows that the satisfiability problems for a bounded fragment of probabilistic CTL (called bounded PCTL) and an extension of the modal $\mu$-calculus with probabilistic quantification over next-modalities (called \pmtl) are decidable. For bounded PCTL, we provide an \nexp-algorithm for the satisfiability problem and show that the logic has a \emph{small model property} where the model size is independent from the probability bounds in the formula. We show that the satisfiability problem of a simple sub-logic of bounded PCTL is PSPACE-complete. We prove that P$\mu$TL has a small model property and that a decision procedure using 2 player parity games can be employed for the satisfiability problem of P$\mu$TL. These results imply that \pmtl\ and qualitative PCTL formulas with only thresholds ${>}0$ and ${=}1$---are incomparable.

ABSTRACT. Hidden Markov Chains (HMCs) are commonly used mathematical models of probabilistic systems. They are employed in various fields such as speech recognition, signal processing, and biological sequence analysis. Motivated by an application in stochastic runtime verification, we consider the problem of distinguishing two given HMCs based on a single observation sequence that one of the HMCs generates. More precisely, given two HMCs and an observation sequence, a distinguishing algorithm is expected to identify the HMC that generates the observation sequence. Two HMCs are called distinguishable if for every epsilon > 0 there is a distinguishing algorithm whose error probability is less than epsilon. We show that one can decide in polynomial time whether two HMCs are distinguishable. Further, we present and analyze two distinguishing algorithms for distinguishable HMCs. The first algorithm makes a decision after processing a fixed number of observations, and it exhibits two-sided error. The second algorithm processes an unbounded number of observations, but the algorithm has only one-sided error. The error probability, for both algorithms, decays exponentially with the number of processed observations. We also provide an algorithm for distinguishing multiple HMCs.

ABSTRACT. Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider.

ABSTRACT. We introduce a new decidable fragment of first-order logic with equality which strictly generalizes two already well-known ones --- the Bernays--Sch\"onfinkel--Ramsey (BSR) Fragment and the Monadic Fragment. The defining principle is the syntactic separation of universally quantified variables from existentially quantified ones at the level of atoms. Thus, our classification neither rests on restrictions of quantifier prefixes (as in the BSR case) nor on restrictions on the arity of predicate symbols (as in the monadic case).

We show that the new fragment exhibits the finite model property and derive a non-elementary upper bound on the computing time required for deciding satisfiability in the new fragment. For the subfragment of prenex sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the satisfiability problem is shown to be complete for NEXPTIME. Finally, we discuss how automated reasoning procedures for can take advantage of our results.

ABSTRACT. A non-deterministic recursive scheme generates a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences; in particular it gives an algorithm to compute the downward closure of the word language given by a non-deterministic higher-order recursive scheme.

ABSTRACT. We study an extension of FO²[<], first-order logic interpreted in finite words in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, 'the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.

We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We also give an effective necessary condition, in terms of the syntactic monoid of a regular language, for a property to be expressible in this logic. We show that this condition is also sufficient for words over a two-letter alphabet. This algebraic analysis allows us to prove, among other things, that our new logic has strictly less expressive power than full first-order logic FO[<].

ABSTRACT. Quiescent consistency is a notion of correctness for a concurrent object that gives meaning to the object’s behaviours in quiescent states, i.e., states in which none of the object’s operations are being executed. The condition enables greater flexibility in object design by allowing more behaviours to be admitted, which in turn allows the algorithms implementing quiescent consistent objects to become more efficient (when executed in a multithreaded environment).

Quiescent consistency of an implementation object is defined in terms of a corresponding abstract specification. This gives rise to two important verification questions: membership (checking whether a behaviour of the implementation is allowed by the specification) and correctness (checking whether all behaviours of the implementation are allowed by the specification). In this paper, we consider the membership and correctness conditions for quiescent consistency, as well as a restricted form that assumes an upper limit on the number of events between two quiescent states. We show that the membership problem for unrestricted quiescent consistency is NP-complete and that the correctness problem is decidable, coNP-hard, and in EXPSPACE. For the restricted form, we show that membership is in PTIME, while correctness is in PSPACE.

ABSTRACT. We study versions of second-order bounded arithmetic where induction and comprehension formulae are positive or where the underlying logic is intuitionistic, examining their relationships to monotone and deep inference proof systems for propositional logic. Both settings induce a distinction between polynomial induction (PIND) and usual induction (IND) independent of quantifier complexity, namely due to the restrictions on negation/implication, and we exploit this to distinguish systems at the propositional level.

In the monotone setting a restriction of the Paris-Wilkie (PW) translation immediately induces quasipolynomial-size monotone propositional proofs from Pi^0_1 arithmetic theorems, as expected. We further show that, when only PIND is used, quasipolynomial-size normal deep inference proofs may be obtained, via a graph-rewriting normalisation procedure from earlier work.

For the intuitionistic setting we calibrate the PW translation with the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic implication. This induces a hierarchy of propositional systems that includes monotone proofs. We show that these theories are powerful enough to prove converse results, namely the soundness of their respective propositional systems, thereby establishing a full correspondence.

ABSTRACT. In this article we study Goedel's functional interpretation from the perspective of learning. We define the notion of a learning algorithm, and show that intuitive realizers to the functional interpretation of both induction and various comprehension schemas can be given in terms these algorithms. In the case of arithmetical comprehension, we clarify how our learning realizers compare to those obtained traditionally using bar recursion, demonstrating that bar recursive interpretations of comprehension correspond to `forgetful' learning algorithms. The main purpose of this work is to gain a deeper insight into the semantics of programs extracted using the functional interpretation. However, in doing so we also aim to better understand how the interpretation relates to other computational interpretations of classical logic for which the notion of learning is inbuilt, such as Hilbert's epsilon calculus or the more recent learning-based realizability interpretations of Aschieri and Berardi.

ABSTRACT. Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of their new extended Frege system, denoted EF+red, which is a natural extension of classical extended Frege EF.

Our main results are the following:

Firstly, we prove that the standard Gentzen-style system G_1^* p-simulates EF+red and that G_1^* is strictly stronger under standard complexity-theoretic hardness assumptions.

Secondly, we show a correspondence of EF+red to bounded arithmetic: EF+red can be seen as the non-uniform propositional version of intuitionistic S^1_2. Specifically, intuitionistic S^1_2 proofs of arbitrary statements in prenex form translate to polynomial-size EF+red proofs, and EF+red is in a sense the weakest system with this property.

Finally, we show that unconditional lower bounds for EF+red would imply either a major breakthrough in circuit complexity or in classical proof complexity, and in fact the converse implications hold as well. Therefore, the system EF+red naturally unites the central problems from circuit and proof complexity.

Technically, our results rest on a formalised strategy extraction theorem for EF+red akin to witnessing in intuitionistic S^1_2 and a normal form for EF+red proofs.

ABSTRACT. This paper modifies our previous work in combining classical logic with intuitionistic logic \cite{liang13apal,liang13lics} to also include affine linear logic, resulting in a system that we call Affine Control Logic. A propositional system with six binary connectives is defined and given a phase space interpretation. Choosing classical, intuitionistic or affine reasoning is entirely dependent on the subformula property. Moreover, the connectives of these logics can mix without restriction. We give a sound and complete sequent calculus that requires novel proof transformations for cut elimination. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. One of our goals is to allow non-classical restrictions to coexist with computational interpretations of classical logic such as found in the lambda-mu calculus. In fact, we show that the transition between different modes of proof, classical, intuitionistic and affine, can be interpreted by delimited control operators. We also discuss how to extend the definition of focused proofs to this logic.

ABSTRACT. We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.

ABSTRACT. We study the FO model checking problem of dense graph classes, namely those which are FO-interpretable in some sparse graph classes. Note that if an input dense graph is given together with the corresponding FO interpretation in a sparse graph, one can easily solve the model checking problem using the existing algorithms for sparse graph classes. However, if the assumed interpretation is not given, then the situation is markedly harder. In this paper we give a structural characterization of graph classes which are FO interpretable in graph classes of bounded degree. This characterization allows us to efficiently compute such an interpretation for an input graph. As a consequence, we obtain an FPT algorithm for FO model checking of graph classes FO interpretable in graph classes of bounded degree. The approach we use to obtain these results may also be of independent interest.

ABSTRACT. Correct operation of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges which are addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards ``the good thing'' rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by *any number* of threads, and the desired liveness properties must hold no matter how many threads are active in the system.

ABSTRACT. Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental ω-regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives; (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical ω-regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives.

ABSTRACT. We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh image.

For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial algorithm and prove a completeness result: we construct a sequence of OCA that admits a polynomial-time algorithm iff there is one for all OCA.

For all three abstractions, it was previously unknown if appropriate NFA of sub-exponential size exist.

ABSTRACT. Automata-logic connections are pillars of the theory of regular languages. Such connections are harder to obtain for transducers, but important results have been obtained recently for word-to-word transformations, showing that the three following models are equivalent: deterministic two-way transducers, monadic second-order (MSO) transducers, and deterministic one-way automata equipped with a finite number of registers. Nested words are words with a nesting structure, allowing to model unranked trees as their depth-first-search linearisations. In this paper, we consider transformations from nested words to words, allowing in particular to produce unranked trees if output words have a nesting structure. The model of visibly pushdown transducers allows to describe such transformations, and we propose a simple deterministic extension of this model with two-way moves that has the following properties: i) it is a simple computational model, that naturally has a good evaluation complexity; ii) it is expressive: it subsumes nested word-to-word MSO transducers, and the exact expressiveness of MSO transducers is recovered using a simple syntactic restriction; iii) it has good algorithmic/closure properties: the model is closed under composition with a one-way letter-to-letter transducer which gives closure under regular look-around, and has a decidable equivalence problem.

ABSTRACT. This article is inspired by two works from the early 90s. The first one is by Bogaert and Tison who considered a model of automata on finite ranked trees where one can check equality and disequality constraints between direct subtrees: they proved that this class of automata is closed under Boolean operations and that both the emptiness and the finiteness problem of the accepted language are decidable. The second one is by Niwinski who showed that one can compute the cardinality of any ω-regular language of infinite trees.

Here, we generalise the model of automata of Tison and Bogaert to the setting of infinite binary trees. Roughly speaking we consider parity tree automata where some transitions are guarded and can be used only when the two direct sub-trees of the current node are equal/disequal. We show that the resulting class of languages encompasses the one of ω-regular languages of infinite trees while sharing most of its closure properties, in particular it is a Boolean algebra. Our main technical contribution is then to prove that it also enjoys decidable emptiness and finiteness problems.

ABSTRACT. A program is interpreted as a collection of resource terms by the Taylor expansion, as a collection of plays by game semantics, and as a collection of types by a non-idempotent intersection type assignment system. This paper investigates the connection between these models and aims to show that they are essentially the same in a certain sense. Technically we study the relational interpretations of resource terms and of plays, which can be seen as non-idempotent intersection type assignment systems for resource terms and plays, respectively, and show that the relational interpretations are injective, have the same image, and respect the compositions. This result allows us to study a property of the game model by using the syntax of a resource calculus and vice versa.

ABSTRACT. Graph games provide the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic reactive processes, the traditional model is perfect-information stochastic games, where some transitions of the game graph are controlled by two adversarial players, and the other transitions are executed probabilistically. We consider such games where the objective is the conjunction of several quantitative objectives (specified as mean-payoff conditions), which we refer to as generalized mean-payoff objectives. The basic decision problem asks for the existence of a finite- or infinite-memory strategy for a player that ensures the generalized mean-payoff objective be satisfied with a desired probability against all strategies of the opponent. A special case of the decision problem is the almost-sure problem where the desired probability is 1. Previous results presented a semi-decision procedure for \epsilon-approximations of the almost-sure problem. In this work, we show that both the almost-sure problem as well as the general basic decision problem are coNP-complete, significantly improving the previous results. Moreover, we show that in the case of 1-player stochastic games, randomized memoryless strategies are sufficient and the problem can be solved in polynomial time. In contrast, in two-player stochastic games, we show that, even with randomized strategies, exponential memory is required in general. Our results are relevant in the synthesis of stochastic reactive systems with multiple quantitative requirements.

ABSTRACT. We introduce games with (bound) guess actions. These are games in which the players may be asked along the play to provide numbers that need to satisfy some bounding constraints. These are natural extensions of domination games occurring in the regular cost function theory. In this paper we consider more specifically the case where the constraints to be bounded are regular cost functions, and the long term goal is an $\omega$-regular winning condition. We show that such games are decidable on finite arenas.