this book constitutes the proceedings of the 17thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2014, held as part of the European Joint conferences on theory and Prac...
详细信息
ISBN:
(数字)9783642548307
ISBN:
(纸本)9783642548291
this book constitutes the proceedings of the 17thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2014, held as part of the European Joint conferences on theory and Practice of software, ETAPS 2014, which took place in Grenoble, France, in April 2014. the 28 papers included in this book, together with one invited talk, were selected from 106 full-paper submissions. the following topical areas are covered: probabilistic systems, semantics of programming languages, networks, program analysis, games and synthesis, compositional reasoning, bisimulation, categorical and algebraic models and logics of programming.
We extend the concept of a synchronizing word from deterministic finite-state automata (DFA) to nested word automata (NWA): A well-matched nested word is called synchronizing if it resets the control state of any conf...
详细信息
ISBN:
(纸本)9783662496305;9783662496299
We extend the concept of a synchronizing word from deterministic finite-state automata (DFA) to nested word automata (NWA): A well-matched nested word is called synchronizing if it resets the control state of any configuration, i.e., takes the NWA from all control states to a single control state. We show that although the shortest synchronizing word for an NWA, if it exists, can be (at most) exponential in the size of the NWA, the existence of such a word can still be decided in polynomial time. As our main contribution, we show that deciding the existence of a short synchronizing word (of at most given length) becomes PSPACE-complete (as opposed to NP-complete for DFA). the upper bound makes a connection to pebble games and Strahler numbers, and the lower bound goes via small-cost synchronizing words for DFA, an intermediate problem that we also show PSPACE-complete. We also characterize the complexity of a number of related problems, using the observation that the intersection nonemptiness problem for NWA is EXP-complete.
Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the ...
详细信息
ISBN:
(纸本)3540212981
Message sequence charts (MSC) are a graphical language for the description of communication scenarios between asynchronous processes. Our starting point is to model systems using an assume-guarantee formalism, in the style of LSCs and Triggered MSCs. We enrich MSCs withthe possibility of using gaps (template MSC), and show their ex-pressivity. this formalism also allows to express logical formulas. We analyze the model-checking problem, whose complexity is linear in the size of the system, and ranges from PTIME to EXPSPACE in the size of the template formula.
this book constitutes the proceedings of the 18thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2015, held in London, UK, in April 2015, as part of the European Joint ...
详细信息
ISBN:
(数字)9783662466780
ISBN:
(纸本)9783662466773
this book constitutes the proceedings of the 18thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2015, held in London, UK, in April 2015, as part of the European Joint conferences on theory and Practice of software, ETAPS 2015.;the 28 full papers presented in this volume were carefully reviewed and selected from 93 submissions. they are organized in topical sections named: semantics of programming languages; categorical models and logics; concurrent, probabilistic and timed systems; automata, games, verification; logical aspects of computational complexity; and type theory, proof theory and implicit computational complexity. the book also contains one full paper invited talk.
We present a new formulation for tree-tuple synchronized languages, much simpler than the existing one. this new formulation allows us to prove stronger structural results. As a consequence, synchronized languages giv...
详细信息
We define nominal equational problems of the form E (W) over bar for all(Y) over bar : P, where P consists of conjunctions and disjunctions of equations s approximate to(alpha) t, freshness constraints a#t and their n...
详细信息
ISBN:
(数字)9783030719951
ISBN:
(纸本)9783030719951;9783030719944
We define nominal equational problems of the form E (W) over bar for all(Y) over bar : P, where P consists of conjunctions and disjunctions of equations s approximate to(alpha) t, freshness constraints a#t and their negations: s not approximate to(alpha) t and a # t, where a is an atom and s, t nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. these results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo alpha-equality) is decidable.
Groupoidal relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. In this pa...
详细信息
Groupoidal relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. In this paper, we develop the theory of GRPOs further, proving that well-known equivalences, other than bisimulation, are congruences. To demonstrate the type of category theoretic arguments which are inherent in the 2-categorical approach, we construct GRPOs in a category of 'bunches and wirings.' Finally, we prove that the 2-categorical theory of GRPOs is a generalisation of the approaches based on Milner's precategories and Leifer's functorial reactive systems. (c) 2004 Elsevier B.V. All rights reserved.
We investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. More precisely, we study expressiveness of the pure and public ambient calculus from...
详细信息
We investigate expressiveness of a fragment of the ambient calculus, a formalism for describing distributed and mobile computations. More precisely, we study expressiveness of the pure and public ambient calculus from which the capability open has been removed, in terms of the reachability problem of the reduction relation. Surprisingly, we show that even for this very restricted fragment, the reachability problem is not decidable. At a second step, for a slightly weaker reduction relation, we prove that reachability can be decided by reducing this problem to markings reachability for Petri nets. Finally, we show that the name-convergence problem as well as the model-checking problem rum out to be unclecidable for boththe original and the weaker reduction relation. (c) 2004 Elsevier B.V. All rights reserved.
this paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family...
详细信息
ISBN:
(纸本)9783031572302;9783031572319
this paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages (L-n) n >= 1 such that Ln can be expressed with a pure future formula of size O(n), but it requires formulae of size 2(Omega(n)) to be captured with past formulae. As a by-product, such a succinctness result shows the optimality of the pastification algorithm proposed in [Artale et al., KR, 2023]. We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in [Markey, Bull. EATCS, 2003]. In place of this method, we devise and apply a combinatorial proof system whose deduction trees represent LTL formulae. the system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness of CTL.
暂无评论