Authors:Mohammad Mahdi Jaghoori; Frank de Boer; Delphine Longuet; Tom Chothia; Marjan Sirjani Pages: 343 - 378 Abstract: Abstract We present an extension of the actor model with real-time, including deadlines associated with messages, and explicit application-level scheduling policies, e.g.,“earliest deadline first” which can be associated with individual actors. Schedulability analysis in this setting amounts to checking whether, given a scheduling policy for each actor, every task is processed within its designated deadline. To check schedulability, we introduce a compositional automata-theoretic approach, based on maximal use of model checking combined with testing. Behavioral interfaces define what an actor expects from the environment, and the deadlines for messages given these assumptions. We use model checking to verify that actors match their behavioral interfaces. We extend timed automata refinement with the notion of deadlines and use it to define compatibility of actor environments with the behavioral interfaces. Model checking of compatibility is computationally hard, so we propose a special testing process. We show that the analyses are decidable and automate the process using the Uppaal model checker. PubDate: 2017-06-01 DOI: 10.1007/s00236-015-0254-x Issue No:Vol. 54, No. 4 (2017)

Authors:Lila Kari; Manasi S. Kulkarni Pages: 379 - 398 Abstract: Abstract The concepts of pseudo-bordered and pseudo-unbordered words are in large part motivated by research in theoretical DNA computing, wherein the Watson–Crick complementarity of DNA strands is modelled as an antimorphic involution, that is, a function \(\theta \) which is an antimorphism, \(\theta (uv)=\theta (v) \theta (u)\) , and an involution, \(\theta (\theta (u))=u\) , for all words u, v over the DNA alphabet. In particular, a word w is said to be \(\theta \) -bordered (or pseudo-bordered) if there exists a word \(v \in \Sigma ^{+}\) that is a proper prefix of w, while \(\theta (v)\) is a proper suffix of w. A word which is not \(\theta \) -bordered is \(\theta \) -unbordered. This paper continues the exploration of properties (for the case where \(\theta \) is a morphic involution) of the set of \(\theta \) -unbordered words, \(D_{\theta }(1)\) , and the sets of words that have exactly i \(\theta \) -borders, \(D_{\theta }(i)\) , \(i \ge 2\) . We prove that, under some conditions, the set \(D_{\theta }(i)\) is disjunctive for all \(i \ge 1\) , and that the set \(D_{\theta }^i(1){\setminus }D(i)\) is disjunctive for all \(i\ge 2\) , where D(i) denotes the set of words with exactly i borders. We also discuss conditions for catenations of languages of \(\theta \) -unbordered words to remain \(\theta \) -unbordered, and anticipate further generalizations by showing that the set of all \(\theta \) -bordered words is not context-free for all morphisms \(\theta \) over an alphabet \(\Sigma \) with \( \Sigma \ge 3\) such that \(\theta (a) \ne a\) for all \(a \in \Sigma \) and \(\theta ^{3}\) equals the identity function on ... PubDate: 2017-06-01 DOI: 10.1007/s00236-016-0258-1 Issue No:Vol. 54, No. 4 (2017)

Authors:Pierpaolo Degano; Gian-Luigi Ferrari; Gianluca Mezzetti Pages: 399 - 433 Abstract: Abstract Two kinds of automata are presented, for recognising new classes of regular and context-free nominal languages. We compare their expressive power with analogous proposals in the literature, showing that they express novel classes of languages. Although many properties of classical languages hold no longer in the nominal case, we design a slight restriction of our models that preserve some interesting ones. In particular, we prove the emptiness problem decidable and we construct the intersection between (restricted) regular and context-free automata. By examples and walking through their properties we argue the relevance of our models in the context of the verification of resource usage patterns. PubDate: 2017-06-01 DOI: 10.1007/s00236-016-0261-6 Issue No:Vol. 54, No. 4 (2017)

Authors:Bogdan Aman; Gabriel Ciobanu Pages: 435 - 445 Abstract: Abstract Recently we have considered the possibility of using bio-inspired mobility for solving a weak NP-complete problem (Partition). In this paper we provide a semi-uniform polynomial solution for a strong NP-complete problem (Bin Packing) by means of membrane computing techniques. The solution employs mobile membranes and elementary membrane division. PubDate: 2017-06-01 DOI: 10.1007/s00236-016-0264-3 Issue No:Vol. 54, No. 4 (2017)

Authors:Filippo Bonchi; Daniela Petrişan; Damien Pous; Jurriaan Rot Pages: 127 - 190 Abstract: Abstract Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. The fact that bisimulations up to context can be safely used in any language specified by GSOS rules can also be seen as an instance of our framework, using the well-known observation by Turi and Plotkin that such languages form bialgebras. In the second part of the paper, we provide a new categorical treatment of weak bisimilarity on labeled transition systems and we prove the soundness of up-to context for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. The weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend the categorical framework developed in the first part to an ordered setting. PubDate: 2017-03-01 DOI: 10.1007/s00236-016-0271-4 Issue No:Vol. 54, No. 2 (2017)

Authors:Javier Esparza; Pierre Ganty; Jérôme Leroux; Rupak Majumdar Pages: 191 - 215 Abstract: Abstract Population protocols (Angluin et al. in PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the computational power of well-specified protocols has been extensively studied, the two basic verification problems remain open: Is a given protocol well specified? Does a given protocol compute a given predicate? We prove that both problems are decidable by reduction to the reachability problem of Petri nets. We also give a new proof of the fact that the predicates computed by well-defined protocols are those definable in Presburger arithmetic (Angluin et al. in PODC, 2006). PubDate: 2017-03-01 DOI: 10.1007/s00236-016-0272-3 Issue No:Vol. 54, No. 2 (2017)

Authors:Paul Hunter; Guillermo A. Pérez; Jean-François Raskin Pages: 3 - 39 Abstract: Abstract Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (1) unrestricted, (2) limited to positional strategies, or (3) limited to word strategies, and show that the two last cases have natural modelling applications. These results apply for quantitative games defined with the classical payoff functions \(\mathsf {Inf}\) , \(\mathsf {Sup}\) , \({\mathsf {LimInf}}\) , \(\mathsf {LimSup}\) , and mean-payoff. We also show that our notion of regret minimization in which Adam is limited to word strategies generalizes the notion of good for games introduced by Henzinger and Piterman, and is related to the notion of determinization by pruning due to Aminof, Kupferman and Lampert. PubDate: 2017-02-01 DOI: 10.1007/s00236-016-0268-z Issue No:Vol. 54, No. 1 (2017)

Authors:Romain Brenguier; Jean-François Raskin; Ocan Sankur Pages: 41 - 83 Abstract: In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. This rule is based on the notion of admissible strategies. We compare this rule with previous rules defined in the literature, and show that contrary to the previous proposals, it defines sets of solutions which are rectangular. This property leads to solutions which are robust and resilient, and allows one to synthesize strategies separately for each agent. We provide algorithms with optimal complexity and also an abstraction framework compatible with the new rule. PubDate: 2017-02-01 DOI: 10.1007/s00236-016-0273-2 Issue No:Vol. 54, No. 1 (2017)

Authors:Thomas Brihaye; Gilles Geeraerts; Axel Haddad; Benjamin Monmege Pages: 85 - 125 Abstract: Abstract Quantitative games are two-player zero-sum games played on directed weighted graphs. Total-payoff games—that can be seen as a refinement of the well-studied mean-payoff games—are the variant where the payoff of a play is computed as the sum of the weights. Our aim is to describe the first pseudo-polynomial time algorithm for total-payoff games in the presence of arbitrary weights. It consists of a non-trivial application of the value iteration paradigm. Indeed, it requires to study, as a milestone, a refinement of these games, called min-cost reachability games, where we add a reachability objective to one of the players. For these games, we give an efficient value iteration algorithm to compute the values and optimal strategies (when they exist), that runs in pseudo-polynomial time. We also propose heuristics to speed up the computations. PubDate: 2017-02-01 DOI: 10.1007/s00236-016-0276-z Issue No:Vol. 54, No. 1 (2017)

Authors:Raymond Devillers Abstract: Abstract It is well-known that the reachability graph of a sum of disjoint Petri nets is the disjoint product of the reachability graphs of the components. We shall consider here the converse problem, i.e., determine when and how a transition system may be decomposed in non-trivial concurrent factors, and extend the theory to more general labelled transition systems. Meanwhile, we shall develop interesting algebraic properties of disjoint products. The present paper is an extended version of Devillers (in: Desel, Yakovlev (eds) Proceedings 16th international conference on application of concurrency to system design (ACSD 2016), 2016). PubDate: 2017-04-29 DOI: 10.1007/s00236-017-0300-y

Authors:Dmitry Chistikov; Rayna Dimitrova; Rupak Majumdar Abstract: 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-04-12 DOI: 10.1007/s00236-017-0297-2

Authors:Roberto Barbuti; Roberta Gori; Francesca Levi; Paolo Milazzo Abstract: Abstract Reaction systems are a qualitative formalism for the modelling of systems of biochemical reactions. In their original formulation, a reaction system executes in an environment (or context) that can supply it with new objects at each evolution step. The context drives the behaviour of a reaction system: it can provide different inputs to the system that can lead to different behaviours. In order to more faithfully deal with open systems, in this paper we propose a more powerful notion of context having not only the capability to provide objects, but also to absorb (or remove) objects at each evolution step. For such reaction systems with generalized context we investigate properties of dynamic causality by revising the previously proposed concept of formula based predictor. A formula based predictor is a Boolean formula characterising all contexts that lead to the production of a certain object after a given number of steps. In this paper, we revise the theory of formula based predictors in order to deal with reaction systems executed in a context of the new kind. As applications, we show an example of interaction between biochemical pathways and a reaction system modelling cell metabolism and respiration. PubDate: 2017-03-28 DOI: 10.1007/s00236-017-0296-3

Authors:David Basin; Felix Klaedtke; Eugen Zălinescu Abstract: Abstract Real-time logics are popular specification languages for reasoning about systems intended to meet timing constraints. Numerous formalisms have been proposed with different underlying time models that can be characterized along two dimensions: dense versus discrete time and point-based versus interval-based. We present monitoring algorithms for the past-only fragment of metric temporal logics that differ along these two dimensions, analyze their complexity, and compare them on a class of formulas for which the point-based and the interval-based settings coincide. Our comparison reveals similarities and differences between the monitoring algorithms and highlights key concepts underlying our and prior monitoring algorithms. For example, point-based algorithms are conceptually simpler and more efficient than interval-based ones as they are invoked only at time points occurring in the monitored trace and their reasoning is limited to just those time points. PubDate: 2017-03-03 DOI: 10.1007/s00236-017-0295-4

Authors:Susmit Jha; Sanjit A. Seshia Abstract: 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-02-15 DOI: 10.1007/s00236-017-0294-5

Authors:Dimitrios Kouzapas; Jorge A. Pérez; Nobuko Yoshida Abstract: Abstract For higher-order (process) languages, characterising contextual equivalence is a long-standing issue. In the setting of a higher-order \(\pi \) -calculus with session types, we develop characteristic bisimilarity, a typed bisimilarity which fully characterises contextual equivalence. To our knowledge, ours is the first characterisation of its kind. Using simple values inhabiting (session) types, our approach distinguishes from untyped methods for characterising contextual equivalence in higher-order processes: we show that observing as inputs only a precise finite set of higher-order values suffices to reason about higher-order session processes. We demonstrate how characteristic bisimilarity can be used to justify optimisations in session protocols with mobile code communication. PubDate: 2016-12-24 DOI: 10.1007/s00236-016-0289-7

Authors:Sadegh Esmaeil Zadeh Soudjani; Alessandro Abate; Rupak Majumdar Abstract: We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of the given Markov processes. Our abstraction differs from existing approaches in two ways: first, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension; second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, approaches which represent and store the (exponentially large) Markov chain explicitly incur significantly higher memory requirements. In our experiments, explicit representations scaled to models of dimension less than half the size as those analyzable by DBN representations. We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property—the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes. PubDate: 2016-12-03 DOI: 10.1007/s00236-016-0287-9

Authors:Marco Carbone; Fabrizio Montesi; Carsten Schürmann; Nobuko Yoshida Abstract: Abstract We propose a Curry–Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence. PubDate: 2016-11-16 DOI: 10.1007/s00236-016-0285-y