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:Kingshuk Chatterjee; Kumar Sankar Ray Pages: 487 - 499 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: 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: 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: 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: 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: 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: 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: 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: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: 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: #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: 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: 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: 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: 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