Abstract: Abstract We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within the state-of-the-art automata-based WS1S decision procedure implemented e.g. in Mona. The way in which the standard decision procedure processes quantifiers involves determinization, with its worst case exponential complexity, for every quantifier alternation in the prefix of a formula. Our algorithm avoids building the deterministic automata—instead, it constructs only those of their states needed for (dis)proving validity of the formula. It uses a symbolic representation of the states, which have a deeply nested structure stemming from the repeated implicit subset construction, and prunes the search space by a nested subsumption relation, a generalization of the one used by the so-called antichain algorithms for handling nondeterministic automata. We have obtained encouraging experimental results, in some cases outperforming Mona, and some of the other recently proposed approaches, by several orders of magnitude. PubDate: 2019-04-01

Abstract: Distributed systems are often organized in chains of components (e.g. business process chains), where each component naturally has a double-sided (left and right) interface. We suggest a corresponding, highly abstract and general framework (in mathematical terms: a monoid) of components and their composition, with minimal assumptions on the underlying global infrastructure (in fact, just a global set of symbols). As a fundamental property, decisive for the composition of more than two components, composition of such properties turns out to be associative. We discuss a number of instantiations of this framework (mainly classes of Petri nets), some of which preserve important properties (such as soundness of workflows) under composition. We glance at a number of generalizations and specializations. PubDate: 2019-04-01

Abstract: Abstract We propose a calculus for concurrent reversible multiparty sessions, equipped with a flexible choice operator allowing for different sets of participants in each branch. This operator is inspired by the notion of connecting action recently introduced by Hu and Yoshida to describe protocols with optional participants. We argue that this choice operator allows for a natural description of typical communication protocols. Our calculus also supports a compact representation of the history of processes and types, which facilitates the definition of rollback. Moreover, it implements a fine-tuned strategy for backward computation. We present a session type system for the calculus and show that it enforces the expected properties of session fidelity, forward progress and backward progress. PubDate: 2019-03-01

Abstract: Turi and Plotkin introduced an elegant approach to structural operational semantics based on universal coalgebra, parametric in the type of syntax and the type of behaviour. Their framework includes abstract GSOS, a categorical generalisation of the classical GSOS rule format, as well as its categorical dual, coGSOS. Both formats are well behaved, in the sense that each specification has a unique model on which behavioural equivalence is a congruence. Unfortunately, the combination of the two formats does not feature these desirable properties. We show that monotone specifications—that disallow negative premises—do induce a canonical distributive law of a monad over a comonad, and therefore a unique, compositional interpretation. PubDate: 2019-02-22

Abstract: 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: 2019-02-01

Abstract: 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: 2019-02-01

Abstract: 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: 2018-12-01

Abstract: 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: 2018-12-01

Abstract: 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: 2018-12-01

Abstract: 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: 2018-12-01

Abstract: Abstract We present a simple model, called depleatable channels, of multi-hop communication in ad hoc networks. We introduce a model for channel energy consumption, and we propose a notion of channel equivalence based on the communication service they provide, regardless of specific routing protocols. In particular, we consider equivalent two channels with identical maximum and minimum inhibiting flow, and prove that this notion of equivalence, and variants of it, coincide with standard equivalences borrowed from the theory of concurrency. Unfortunately, while the maximum flow can be computed in polynomial time, calculating the value of a minimum inhibiting flow is NP-hard. Thus, we propose a characterization of those graphs, called weak, which admit charge assignments for which the minimum inhibiting flow is strictly less than the maximum flow and show that weakness can be checked efficiently by providing an algorithm that does so in polynomial time. PubDate: 2018-11-08

Abstract: 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: 2018-11-01

Abstract: 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: 2018-11-01

Authors:Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja Abstract: Abstract We study the hardness of deciding probabilistic termination as well as the hardness of approximating expected values (e.g. of program variables) and (co)variances for probabilistic programs. Termination We distinguish two notions of probabilistic termination: Given a program P and an input \(\sigma \) ... ...does P terminate with probability 1 on input \(\sigma \) ' (almost-sure termination) ...is the expected time until P terminates on input \(\sigma \) finite' (positive almost-sure termination) For both of these notions, we also consider their universal variant, i.e. given a program P, does P terminate on all inputs' We show that deciding almost-sure termination as well as deciding its universal variant is \(\varPi ^0_2\) -complete in the arithmetical hierarchy. Deciding positive almost-sure termination is shown to be \(\varSigma _2^0\) -complete, whereas its universal variant is \(\varPi _3^0\) -complete. Expected values Given a probabilistic program P and a random variable f mapping program states to rationals, we show that computing lower and upper bounds on the expected value of f after executing P is \(\varSigma _1^0\) - and \(\varSigma _2^0\) -complete, respectively. Deciding whether the expected value equals a given rational value is shown to be \(\varPi ^0_2\) -complete. Covariances We show that computing upper and lower bounds on the covariance of two random variables is both \(\varSigma _2^0\) -complete. Deciding whether the covariance equals a given rational value is shown to be in \(\varDelta _3^0\) . In addition, this problem is shown to be \(\varSigma ^0_2\) -hard as well as \(\varPi ^0_2\) -hard and thus a “proper” \(\varDelta _3^0\) -problem. All hardness results on covariances apply to variances as well. PubDate: 2018-05-15 DOI: 10.1007/s00236-018-0321-1

Authors:Jörg Desel; Javier Esparza; Philipp Hoffmann Abstract: Abstract This paper introduces negotiations, a model of concurrency close to Petri nets, with multi-party negotiations as concurrency primitive. We study two fundamental analysis problems. The soundness problem consists in deciding if it is always possible for a negotiation to terminate successfully, whatever the current state is. Given a sound negotiation, the summarization problem aims at computing an equivalent one-step negotiation with the same input/output behavior. The soundness and summarization problems can be solved by means of simple algorithms acting on the state space of the negotiation, which however face the well-known state explosion problem. We study alternative algorithms that avoid the construction of the state space. In particular, we define reduction rules that simplify a negotiation while preserving the sound/non-sound character of the negotiation and its summary. In a first result we show that our rules are complete for the class of weakly deterministic acyclic negotiations, meaning that they reduce all sound negotiations in this class, and only them, to equivalent one-step negotiations. This provides algorithms for both the soundness and the summarization problem that avoid the construction of the state space. We then study the class of deterministic negotiations. Our second main result shows that the rules are also complete for this class, even if the negotiations contain cycles. Moreover, we present an algorithm that completely reduces all sound deterministic negotiations, and only them, in polynomial time. PubDate: 2018-03-20 DOI: 10.1007/s00236-018-0318-9

Authors:Rosa Abbasi; Fatemeh Ghassemi; Ramtin Khosravi Abstract: Abstract Component-based systems evolve as a new component is added or an existing one is replaced by a newer version. Hence, it is appealing to assure the new system still preserves its safety properties. However, instead of inspecting the new system as a whole, which may result in a large state space, it is beneficial to reuse the verification results by inspecting the newly added component in isolation. To this aim, we study the problem of model checking component-based asynchronously communicating systems in the presence of an unspecified component against safety properties. Our solution is based on assume-guarantee reasoning, adopted for asynchronous environments, which generates the weakest assumption. If the newly added component conforms to the assumption, then the whole system still satisfies the property. To make the approach efficient and convergent, we produce an overapproximated interface of the missing component and by its composition with the rest of the system components, we achieve an overapproximated specification of the system, from which we remove those traces of the system that violate the property and generate an assumption for the missing component. We have implemented our approach on two case studies. Furthermore, we compared our results with the state of the art direct approach. Our resulting assumptions are smaller in size and achieved faster. PubDate: 2018-03-07 DOI: 10.1007/s00236-018-0317-x

Authors:Hongbo Zhang Abstract: 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: 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