Authors:Aaron Bohy; Véronique Bruyère; Jean-François Raskin; Nathalie Bertrand Pages: 545 - 587 Abstract: 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: 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: 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:Kingshuk Chatterjee; Kumar Sankar Ray Pages: 487 - 499 Abstract: Abstract Since 1970, reversible finite automata have generated interest among researcher; but till now, we have not come across a model of reversible read only one-way finite automata which accept all regular languages, In this paper, we introduce a new model of one-way reversible finite automata inspired by the Watson–Crick complementarity relation and show that our model can accept all regular languages. We further show that our model accepts a language which is not accepted by any multi-head deterministic finite automaton. PubDate: 2017-08-01 DOI: 10.1007/s00236-016-0267-0 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: 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: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:Sjoerd Cranen; Jeroen J. A. Keiren; Tim A. C. Willemse Abstract: 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

Authors:Elie Fares; Jean-Paul Bodeveix; Mamoun Filali Abstract: Formal specification languages have a lot of notions in common. They all introduce entities usually called processes, offer similar operators, and most importantly define their operational semantics based on labelled transition systems (LTS). However, each language defines specific synchronizing and/or memory structures. For instance, in CSP, the synchronization is defined between identical events, while in CCS and in synchronization vectors-based views it is defined respectively between complementary events or between possibly different events. In this paper, we aim at capturing some similarities of specification languages by defining a label-based formal framework for reasoning on LTS, their semantics and related properties. Firstly, we define a high-level synchronization mechanism in the form of an abstract label structure and identify some properties. Then, we introduce operators for composing and transforming label structures, study their intrinsic properties and explore how label structure properties propagate. Secondly, we introduce a LTS-based behavioral framework. We then lift the label structure composition and transformation operators to the LTS level and establish LTS-related properties derived from those of their underlying labelled structures. Thirdly, we consider extended transition systems, more specifically timed automata, as LTS built on top of specific labelled structures. Their semantics is reconstructed by applying operators of our framework on the syntactic LTS, which allows the direct proof of some semantic properties such as compositionality. PubDate: 2017-07-18 DOI: 10.1007/s00236-017-0302-9

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: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: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