Authors:Dmitry Chistikov; Rayna Dimitrova; Rupak Majumdar Pages: 729 - 764 Abstract: #SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this paper, we show a reduction from an approximate version of #SMT to SMT. We focus on the theories of integer arithmetic and linear real arithmetic. We propose model counting algorithms that provide approximate solutions with formal bounds on the approximation error. They run in polynomial time and make a polynomial number of queries to the SMT solver for the underlying theory, exploiting “for free” the sophisticated heuristics implemented within modern SMT solvers. We have implemented the algorithms and used them to solve the value problem for a model of loop-free probabilistic programs with nondeterminism. PubDate: 2017-12-01 DOI: 10.1007/s00236-017-0297-2 Issue No:Vol. 54, No. 8 (2017)

Authors:Mirco Giacobbe; Călin C. Guet; Ashutosh Gupta; Thomas A. Henzinger; Tiago Paixão; Tatjana Petrov Pages: 765 - 787 Abstract: The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights. PubDate: 2017-12-01 DOI: 10.1007/s00236-016-0278-x Issue No:Vol. 54, No. 8 (2017)

Authors:Parosh Aziz Abdulla; Stavros Aronis; Mohamed Faouzi Atig; Bengt Jonsson; Carl Leonardsson; Konstantinos Sagonas Pages: 789 - 818 Abstract: We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel representation of executions under TSO and PSO, called chronological traces. Chronological traces induce a partial order relation on relaxed memory executions, capturing dependencies that are needed to represent the interaction via shared variables. They are optimal in the sense that they only distinguish computations that are inequivalent under the widely-used representation by Shasha and Snir. This allows an optimal dynamic partial order reduction algorithm to explore a minimal number of executions while still guaranteeing full coverage. We apply our techniques to check, under the TSO and PSO memory models, LLVM assembly produced for C/pthreads programs. Our experiments show that our technique reduces the verification effort for relaxed memory models to be almost that for the standard model of sequential consistency. This article is an extended version of Abdulla et al. (Tools and algorithms for the construction and analysis of systems, Springer, New York, pp 353–367, 2015), appearing in TACAS 2015. PubDate: 2017-12-01 DOI: 10.1007/s00236-016-0275-0 Issue No:Vol. 54, No. 8 (2017)

Authors:Chung-Hao Huang; Sven Schewe; Farn Wang Pages: 625 - 654 Abstract: We propose a logic for the definition of the collaborative power of groups of agents to enforce different temporal objectives. The resulting temporal cooperation logic (TCL) extends ATL by allowing for successive definition of strategies for agents and agencies. Different to previous logics with similar aims, our extension cuts a fine line between extending the power and maintaining a low complexity: model checking TCL sentences is EXPTIME complete in the logic, and NL complete in the model. This advancement over nonelementary logics is bought by disallowing a too close entanglement between the cooperation and competition. We show how allowing such an entanglement immediately leads to a nonelementary complexity. We have implemented a model checker for the logic and shown the feasibility of model checking on a few benchmarks. PubDate: 2017-11-01 DOI: 10.1007/s00236-016-0277-y Issue No:Vol. 54, No. 7 (2017)

Authors:Takashi Tomita; Atsushi Ueno; Masaya Shimakawa; Shigeki Hagihara; Naoki Yonezaki Pages: 655 - 692 Abstract: Linear temporal logic (LTL) synthesis is a formal method for automatically composing a reactive system that realizes a given behavioral specification described in LTL if the specification is realizable. Even if the whole specification is unrealizable, it is preferable to synthesize a best-effort reactive system. That is, a system that maximally realizes its partial specifications. Therefore, we categorized specifications into must specifications (which should never be violated) and desirable specifications (the violation of which may be unavoidable). In this paper, we propose a method for synthesizing a reactive system that realizes all must specifications and strongly endeavors to satisfy each desirable specification. The general form of the desirable specifications without assumptions is \(\mathbf{G }\varphi \) , which means “ \(\varphi \) always holds”. In our approach, the best effort to satisfy \(\mathbf{G }\varphi \) is to maximize the number of steps satisfying \(\varphi \) in the interaction. To quantitatively evaluate the number of steps, we used a mean-payoff objective based on LTL formulae. Our method applies the Safraless approach to construct safety games from given must and desirable specifications, where the must specification can be written in full LTL and may include assumptions. It then transforms the safety games constructed from the desirable specifications into mean-payoff games and finally composes a reactive system as an optimal strategy on a synchronized product of the games. PubDate: 2017-11-01 DOI: 10.1007/s00236-016-0280-3 Issue No:Vol. 54, No. 7 (2017)

Authors:Susmit Jha; Sanjit A. Seshia Pages: 693 - 726 Abstract: Formal synthesis is the process of generating a program satisfying a high-level formal specification. In recent times, effective formal synthesis methods have been proposed based on the use of inductive learning. We refer to this class of methods that learn programs from examples as formal inductive synthesis. In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how formal inductive synthesis differs from traditional machine learning. We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a family of synthesizers that operate by iteratively querying an oracle. An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS). We present a theoretical characterization of CEGIS for learning any program that computes a recursive language. In particular, we analyze the relative power of CEGIS variants where the types of counterexamples generated by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning algorithm. In the special case where the universe of candidate programs is finite, we relate the speed of convergence to the notion of teaching dimension studied in machine learning theory. Altogether, the results of the paper take a first step towards a theoretical foundation for the emerging field of formal inductive synthesis. PubDate: 2017-11-01 DOI: 10.1007/s00236-017-0294-5 Issue No:Vol. 54, No. 7 (2017)

Authors:Aaron Bohy; Véronique Bruyère; Jean-François Raskin; Nathalie Bertrand Pages: 545 - 587 Abstract: When treating Markov decision processes (MDPs) with large state spaces, using explicit representations quickly becomes unfeasible. Lately, Wimmer et al. have proposed a so-called symblicit algorithm for the synthesis of optimal strategies in MDPs, in the quantitative setting of expected mean-payoff. This algorithm, based on the strategy iteration algorithm of Howard and Veinott, efficiently combines symbolic and explicit data structures, and uses binary decision diagrams as symbolic representation. The aim of this paper is to show that the new data structure of pseudo-antichains (an extension of antichains) provides another interesting alternative, especially for the class of monotonic MDPs. We design efficient pseudo-antichain based symblicit algorithms (with open source implementations) for two quantitative settings: the expected mean-payoff and the stochastic shortest path. For two practical applications coming from automated planning and \(\mathsf {LTL}\) synthesis, we report promising experimental results w.r.t. both the run time and the memory consumption. We also show that a variant of pseudo-antichains allows to handle the infinite state spaces underlying the qualitative verification of probabilistic lossy channel systems. PubDate: 2017-09-01 DOI: 10.1007/s00236-016-0255-4 Issue No:Vol. 54, No. 6 (2017)

Authors:Milan Češka; Frits Dannenberg; Nicola Paoletti; Marta Kwiatkowska; Luboš Brim Pages: 589 - 623 Abstract: We consider the problem of synthesising rate parameters for stochastic biochemical networks so that a given time-bounded CSL property is guaranteed to hold, or, in the case of quantitative properties, the probability of satisfying the property is maximised or minimised. Our method is based on extending CSL model checking and standard uniformisation to parametric models, in order to compute safe bounds on the satisfaction probability of the property. We develop synthesis algorithms that yield answers that are precise to within an arbitrarily small tolerance value. The algorithms combine the computation of probability bounds with the refinement and sampling of the parameter space. Our methods are precise and efficient, and improve on existing approximate techniques that employ discretisation and refinement. We evaluate the usefulness of the methods by synthesising rates for three biologically motivated case studies: infection control for a SIR epidemic model; reliability analysis of molecular computation by a DNA walker; and bistability in the gene regulation of the mammalian cell cycle. PubDate: 2017-09-01 DOI: 10.1007/s00236-016-0265-2 Issue No:Vol. 54, No. 6 (2017)

Authors:A. Marin; S. Rossi Pages: 447 - 485 Abstract: In the literature, the notions of lumpability and time reversibility for large Markov chains have been widely used to efficiently study the functional and non-functional properties of computer systems. In this paper we explore the relations among different definitions of lumpability (strong, exact and strict) and the notion of time-reversed Markov chain. Specifically, we prove that an exact lumping induces a strong lumping on the reversed Markov chain and a strict lumping holds both for the forward and the reversed processes. Based on these results we introduce the class of \(\lambda \rho \) -reversible Markov chains which combines the notions of lumping and time reversibility modulo state renaming. We show that the class of autoreversible processes, previously introduced in Marin and Rossi (Proceedings of the IEEE 21st international symposium on modeling, analysis and simulation of computer and telecommunication systems MASCOTS, pp. 151–160, 2013), is strictly contained in the class of \(\lambda \rho \) -reversible chains. PubDate: 2017-08-01 DOI: 10.1007/s00236-016-0266-1 Issue No:Vol. 54, No. 5 (2017)

Authors:Achour Mostéfaoui; Michel Raynal Pages: 501 - 520 Abstract: This paper presents a new algorithm that reduces multivalued consensus to binary consensus in an asynchronous message-passing system made up of n processes where up to t may commit Byzantine failures. This algorithm has the following noteworthy properties: it assumes \(t<n/3\) (and is consequently optimal from a resilience point of view), uses \(O(n^2)\) messages, has a constant time complexity, and uses neither signatures nor additional computational power (such as random numbers, failure detectors, additional scheduling assumption, or additional synchrony assumption). The design of this reduction algorithm relies on two new all-to-all communication abstractions. The first one allows the non-faulty processes to reduce the number of proposed values to c, where c is a small constant. The second communication abstraction allows each non-faulty process to compute a set of (proposed) values satisfying the following property: if the set of a non-faulty process is a singleton containing value v, the set of any non-faulty process contains v. Both communication abstractions have an \(O(n^2)\) message complexity and a constant time complexity. The reduction of multivalued Byzantine consensus to binary Byzantine consensus is then a simple sequential use of these communication abstractions. To the best of our knowledge, this is the first asynchronous message-passing algorithm that reduces multivalued consensus to binary consensus with \(O(n^2)\) messages and constant time complexity (measured with the longest causal chain of messages) in the presence of up to \(t<n/3\) Byzantine processes, and without using cryptography techniques. Moreover, this reduction algorithm uses a single instance of the underlying binary consensus, and tolerates message re-ordering by Byzantine processes. PubDate: 2017-08-01 DOI: 10.1007/s00236-016-0269-y Issue No:Vol. 54, No. 5 (2017)

Authors:Ke Gu; Weijia Jia; Guojun Wang; Sheng Wen Pages: 521 - 541 Abstract: Attribute-based signature (ABS) is a novel cryptographic primitive, which can make the signing party sign a message with fine-grained control over identifying information. ABS only reveals the fact that the verified message must be signed by a user with a set of attributes satisfying a predicate. Thus, ABS can hide any identifying information and make fine-grained control on signing. Presently, many attribute-based signature schemes have been proposed, but most of them are not very efficient. Maji et al. recently presented a complete definition and construction about ABS for monotone predicates and showed three instantiations under their framework for ABS. Although the most practical one of their instantiations is efficient, the instantiation is constructed in the generic group model and has been proved to be insecure. Then, Okamoto et al. proposed an attribute-based signature scheme in the standard model, which can support generalized non-monotone predicates over access structure. However, their scheme is not efficient in practice. In this paper, we present a framework for ABS and show a detailed security model for ABS. Under our framework, we present an attribute-based signature scheme for monotone predicates in the standard model, where we choose the Waters’ signature scheme as the prototype of our attribute-based signature scheme. Compared with the Maji’s scheme in the generic group model, the proposed scheme is constructed in the standard model. Furthermore, compared with the Okamoto’s scheme, the proposed scheme is more efficient by decreasing the computation cost. PubDate: 2017-08-01 DOI: 10.1007/s00236-016-0270-5 Issue No:Vol. 54, No. 5 (2017)

Authors:Angelo Borsotti; Luca Breveglieri; Stefano Crespi Reghizzi; Angelo Morzenti Abstract: Extended BNF grammars (EBNF) allow regular expressions in the right parts of their rules. They are widely used to define languages, and can be represented by recursive Transition Networks (TN) consisting of a set of finite-state machines. We present a novel direct construction of efficient shift-reduce ELR(1) parsers for TNs. We show that such a parser works deterministically if the TN is free from the classical shift-reduce and reduce–reduce conflicts of the LR(1) parsers, and from a new conflict type called convergence conflict. Such a novel condition for determinism is proved correct and is more general than those proposed in the past for EBNF grammars or TNs. Such ELR(1) parsers perform fewer shift moves than the equivalent LR(1) parsers. A simple optimization of the reduction moves is described. PubDate: 2017-11-04 DOI: 10.1007/s00236-017-0308-3

Authors:Rachel Faran; Orna Kupferman Abstract: Of special interest in formal verification are safety specifications, which assert that the system stays within some allowed region, in which nothing “bad” happens. Equivalently, a computation violates a safety specification if it has a “bad prefix”—a prefix all whose extensions violate the specification. The theoretical properties of safety specifications as well as their practical advantages with respect to general specifications have been widely studied. Safety is binary: a specification is either safety or not safety. We introduce a quantitative measure for safety. Intuitively, the safety level of a language L measures the fraction of words not in L that have a bad prefix. In particular, a safety language has safety level 1 and a liveness language has safety level 0. Thus, our study spans the spectrum between traditional safety and liveness. The formal definition of safety level is based on probability and measures the probability of a random word not in L to have a bad prefix. We study the problem of finding the safety level of languages given by means of deterministic and nondeterministic automata as well as LTL formulas, and the problem of deciding their membership in specific classes along the spectrum (safety, almost-safety, fraction-safety, etc.). We also study properties of the different classes and the structure of deterministic automata for them. PubDate: 2017-10-23 DOI: 10.1007/s00236-017-0307-4

Authors:Chao Wang; Yi Lv; Peng Wu Abstract: TSO-to-TSO linearizability is a variant of linearizability for concurrent libraries on the total store order (TSO) memory model. It is proved in this paper that TSO-to-TSO linearizability for a bounded number of processes is undecidable. We first show that the trace inclusion problem of a classic-lossy single-channel system, which is known undecidable, can be reduced to the history inclusion problem of specific libraries on the TSO memory model. Based on the equivalence between history inclusion and extended history inclusion for these libraries, we then prove that the extended history inclusion problem of libraries is undecidable on the TSO memory model. By means of extended history inclusion as an equivalent characterization of TSO-to-TSO linearizability, we finally prove that TSO-to-TSO linearizability is undecidable for a bounded number of processes. Additionally, we prove that all variants of history inclusion problems are undecidable on TSO for a bounded number of processes. PubDate: 2017-10-23 DOI: 10.1007/s00236-017-0305-6

Authors:Dietmar Berwanger; Anup Basil Mathew; Marie van den Bogaard Abstract: Infinite games with imperfect information are known to be undecidable unless the information flow is severely restricted. One fundamental decidable case occurs when there is a total ordering among players, such that each player has access to all the information that the following ones receive. In this paper we consider variations of this hierarchy principle for synchronous games with perfect recall, and identify new decidable classes for which the distributed synthesis problem is solvable with finite-state strategies. In particular, we show that decidability is maintained when the information hierarchy may change along the play, or when transient phases without hierarchical information are allowed. Finally, we interpret our result in terms of distributed system architectures. PubDate: 2017-10-17 DOI: 10.1007/s00236-017-0306-5

Authors:Paul Hunter; Guillermo A. Pérez; Jean-François Raskin Abstract: Mean-payoff games (MPGs) are infinite duration two-player zero-sum games played on weighted graphs. Under the hypothesis of full observation, they admit memoryless optimal strategies for both players and can be solved in \({\mathsf {NP}}\cap {\mathsf {coNP}}\) . MPGs are suitable quantitative models for open reactive systems. However, in this context the assumption of full observation is not always realistic. For the partial-observation case, the problem that asks if the first player has an observation-based winning strategy that enforces a given threshold on the mean payoff, is undecidable. In this paper, we study the window mean-payoff objectives introduced recently as an alternative to the classical mean-payoff objectives. We show that, in sharp contrast to the classical mean-payoff objectives, some of the window mean-payoff objectives are decidable in games with partial observation. PubDate: 2017-10-11 DOI: 10.1007/s00236-017-0304-7

Authors:Søren Debois; Thomas T. Hildebrandt; Tijs Slaats Abstract: We explore the complexity of reachability and run-time refinement under safety and liveness constraints in event-based process models. Our study is framed in the DCR \(^\star \) process language, which supports modular specification through a compositional operational semantics. DCR \(^\star \) encompasses the “Dynamic Condition Response (DCR) graphs” declarative process model for analysis, execution and safe run-time refinement of process-aware information systems; including replication of sub-processes. We prove that event-reachability and refinement are np-hard for DCR \(^\star \) processes without replication, and that these finite state processes recognise exactly the languages that are the union of a regular and an \(\omega \) -regular language. Moreover, we prove that event-reachability and refinement are undecidable in general for DCR \(^\star \) processes with replication and local events, and we provide a tractable approximation for refinement. A prototype implementation of the DCR \(^\star \) language is available at http://dcr.tools/acta16. PubDate: 2017-09-21 DOI: 10.1007/s00236-017-0303-8

Authors:Sjoerd Cranen; Jeroen J. A. Keiren; Tim A. C. Willemse Abstract: Parity games play a central role in model checking and satisfiability checking. Solving parity games is computationally expensive, among others due to the size of the games, which, for model checking problems, can easily contain \(10^9\) vertices or beyond. Equivalence relations can be used to reduce the size of a parity game, thereby potentially alleviating part of the computational burden. We reconsider (governed) bisimulation and (governed) stuttering bisimulation, and we give detailed proofs that these relations are equivalences, have unique quotients and they approximate the winning regions of parity games. Furthermore, we present game-based characterisations of these relations. Using these characterisations our equivalences are compared to relations for parity games that can be found in the literature, such as direct simulation equivalence and delayed simulation equivalence. To complete the overview we develop coinductive characterisations of direct- and delayed simulation equivalence and we establish a lattice of equivalences for parity games. PubDate: 2017-08-04 DOI: 10.1007/s00236-017-0301-x