Authors:Édouard Bonnet; Vangelis Th. Paschos Pages: 1 - 15 Abstract: Instance sparsification is well-known in the world of exact computation since it is very closely linked to the Exponential Time Hypothesis. In this paper, we extend the concept of sparsification in order to capture subexponential time approximation. We develop a new tool for inapproximability, called approximation preserving sparsification, and use it in order to get strong inapproximability results in subexponential time for several fundamental optimization problems such as min dominating set , min feedback vertex set , min set cover, min feedback arc set, and others. PubDate: 2018-02-01 DOI: 10.1007/s00236-016-0281-2 Issue No:Vol. 55, No. 1 (2018)

Authors:Henrik Björklund; Wim Martens; Thomas Schwentick Pages: 17 - 56 Abstract: We study the containment, satisfiability, and validity problems for conjunctive queries over trees with respect to a schema. We show that conjunctive query containment and validity are 2EXPTIME -complete with respect to a schema, in both cases where the schema is given as a DTD or as a tree automaton. Furthermore, we show that satisfiability for conjunctive queries with respect to a schema can be decided in NP . The problem is NP -hard already for queries using only one kind of axis. Finally, we consider conjunctive queries that can test for equalities and inequalities of data values. Here, satisfiability and validity are decidable, but containment is undecidable, even without schema information. On the other hand, containment with respect to a schema becomes decidable again if the “larger” query is not allowed to use both equalities and inequalities. PubDate: 2018-02-01 DOI: 10.1007/s00236-016-0282-1 Issue No:Vol. 55, No. 1 (2018)

Authors:Lene M. Favrholdt; Jesper W. Mikkelsen Pages: 57 - 80 Abstract: We study a version of online edge coloring, where the goal is to color as many edges as possible using only a given number, k, of available colors. All of our results are with regard to competitive analysis. Previous attempts to identify optimal algorithms for this problem have failed, even for bipartite graphs. Thus, in this paper, we analyze even more restricted graph classes, paths and trees. For paths, we consider \(k=2\) , and for trees, we consider any \(k \ge 2\) . We prove that a natural greedy algorithm called \({\textsc {First-Fit}}\) is optimal among deterministic algorithms, on paths as well as trees. For paths, we give a randomized algorithm, which is optimal and better than the best possible deterministic algorithm. For trees, we prove that to obtain a better competitive ratio than \({\textsc {First-Fit}}\) , the algorithm would have to be both randomized and unfair (i.e., reject edges that could have been colored), and even such algorithms cannot be much better than \({\textsc {First-Fit}}\) . PubDate: 2018-02-01 DOI: 10.1007/s00236-016-0283-0 Issue No:Vol. 55, No. 1 (2018)

Authors:Juha Honkala Pages: 81 - 88 Abstract: We study the language equivalence problem for smooth and loop-free D0L systems. We show that the number of initial terms in the associated D0L sequences we have to consider to decide language equivalence depends only on the cardinality of the underlying alphabet. PubDate: 2018-02-01 DOI: 10.1007/s00236-016-0286-x Issue No:Vol. 55, No. 1 (2018)

Authors:Hongbo Zhang Abstract: In this paper, we analyze an M/M/1 queue with batch arrival and multiple working vacations. We describe the queueing model by a special GI/M/1 type Markov process with infinite phases, and by the matrix analytic method, we not only give the stationary queue length distribution of the model, but also obtain the exact number of vacations completed by the server. PubDate: 2018-02-05 DOI: 10.1007/s00236-018-0316-y

Authors:Henning Fernau; Lakshmanan Kuppusamy; Indhumathi Raman Abstract: A graph-controlled insertion–deletion system is a regulated extension of an insertion–deletion system. It has several components and each component contains some insertion–deletion rules. These components are the vertices of a directed control graph. A transition is performed by any applicable rule in the current component on a string and the resultant string is then moved to the target component specified in the rule. This also describes the arcs of the control graph. Starting from an axiom in the initial component, strings thus move through the control graph. The language of the system is the set of all terminal strings collected in the final component. In this paper, we investigate a variant of the main question in this area: which combinations of size parameters (the maximum number of components, the maximal length of the insertion string, the maximal length of the left context for insertion, the maximal length of the right context for insertion; plus three similar restrictions with respect to deletion) are sufficient to maintain computational completeness of such restricted systems under the additional restriction that the (undirected) control graph is a path' Notice that these results also bear consequences for the domain of insertion–deletion P systems, improving on a number of previous results from the literature, concerning in particular the number of components (membranes) that are necessary for computational completeness results. PubDate: 2018-02-05 DOI: 10.1007/s00236-018-0312-2

Authors:Masoud Ebrahimi; Gholamreza Sotudeh; Ali Movaghar Abstract: Few fuzzy temporal logics and modeling formalisms are developed such that their model checking is both effective and efficient. State-space explosion makes model checking of fuzzy temporal logics inefficient. That is because either the modeling formalism itself is not compact, or the verification approach requires an exponentially larger yet intermediate representation of the modeling formalism. To exemplify, Fuzzy Program Graph (FzPG) is a very compact, and powerful formalism to model fuzzy systems; yet, it is required to be translated into an equal Fuzzy Kripke model with an exponential blow-up should it be formally verified. In this paper, we introduce Fuzzy Computation Tree Logic (FzCTL) and its direct symbolic model checking over FzPG that avoids the aforementioned state-space explosion. Considering compactness and readability of FzPG along with expressiveness of FzCTL, we believe the proposed method is applicable in real-world scenarios. Finally, we study formal verification of fuzzy flip-flops to demonstrate capabilities of the proposed method. PubDate: 2018-02-03 DOI: 10.1007/s00236-018-0311-3

Authors:Paolo Baldan; Fabio Gadducci Abstract: In a seminal paper Montanari and Meseguer have shown that an algebraic interpretation of Petri nets in terms of commutative monoids can be used to provide an elegant characterisation of the deterministic computations of a net, accounting for their sequential and parallel composition. A smoother and more complete theory for deterministic computations has been later developed by relying on the concept of pre-net, a variation of Petri nets with a non-commutative flavor. This paper shows that, along the same lines, by adding an (idempotent) operation and thus considering dioids (idempotent semirings) rather than just monoids, one can faithfully characterise the non-deterministic computations of a net. PubDate: 2018-01-24 DOI: 10.1007/s00236-018-0314-0

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:Cao Chunhua; Lu Qing; Yang Di Abstract: It is always an interesting subject to investigate whether a three-element language is a code or not. In this paper, we consider a special class of three-element languages, where two words have the same length which is less than the length of the third word. We give a necessary and sufficient condition to state whether a three-element language in this class is a code. This result partially resolves the problem proposed by Professor H. J. Shyr in 1990s. PubDate: 2017-11-29 DOI: 10.1007/s00236-017-0309-2

Authors:Eike Best; Raymond Devillers; Uli Schlachter Abstract: This paper describes a synthesis procedure dedicated to the construction of choice-free Petri nets from finite persistent transition systems, whenever possible. Taking advantage of the properties of choice-free Petri nets, a two-step approach is proposed. A pre-synthesis step checks necessary structural properties of the transition system and constructs some data structures needed for the second step. Then, a minimised set of simplified systems of linear inequalities is distilled from a general region-theoretic approach. This leads to a substantial narrowing of the sets of states for which linear inequalities must be solved, and allows an early detection of failures, supported by constructive error messages. The performance of the resulting algorithm is measured and compared numerically with existing synthesis tools. PubDate: 2017-11-20 DOI: 10.1007/s00236-017-0310-9

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