2,933 research outputs found
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory
No full textIn the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i.e., conditions that only refer to individual components.
In this paper, we consider global winning conditions such as mutual exclusion, i.e., conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games
Correctness of programs with Pascal-like procedures without global variables
No full textAbstractWe study a programming language LPas consisting of blockstructured programs with a Pascal-like procedure concept which allows procedures as parameters. Due to Clarke (1979) there cannot be any sound and relatively complete Hoare-like system proving partial correctness for the full language LPas. However, in Langmaack and Olderog (1980) it has been conjectured that such a system exists once global variables are disallowed.In this paper we prove a slightly weaker version of this conjecture by presenting a Hoare-like system which is sound and g-complete for all programs in LPas without global variables; g-completeness means completeness modulo a special second-order theory and an appropriate notion of expressiveness. The proof system provides new methods of dealing with procedures which are formalized in the Rule of Separation for procedure calls. The completeness proof for the system is carried out in a transparent way using modified formal computation trees. An example shows how to apply the proposed methods
Report on WS25CCC Workshop "25 Years of Combining Compositionality and Concurrency"
No full textInternational audienceIn the peak of the summer 2013, between the 7th and the 9th of August, the workshop "25 Years of Combining Compositionality and Concurrency" took place in Königswinter, a picturesque little town overlooking the Rhine river, in the outskirts of Bonn. The event, organised by Ursula Goltz, Rob van Glabbeek and Ernst-Rüdiger Olderog, was meant to celebrate and revisit, a quarter of a century later, the workshop "Combining Compositionality and Concurrency" (CCC88) that had been held in March 1988 in the same hotel, the Loreley, on the initiative of the same trio of researchers (the first two of which were still PhD students at the time). Both workshops were by invitation only, and each attracted 34 participants. Because of its timely character and its deliberate focus on bridging the gap be-tween process calculi and "true-concurrency" models, the original CCC88 workshop, targeting a group of active researchers from both fields, had generated much enthusiasm and discussion. It had therefore gradually acquired, at least in the memories of its participants, the mythical status of a "foundational event". It was then quite natural for the organisers, 25 years later, to envisage a kind of jubilee event, which could bring together a number of participants from the original workshop, as well as younger researchers who had joined in more recent years the field of concurrency theory, now much broader and well-established
Take it NP-easy: Bounded model construction for duration calculus
No full textFollowing the recent successes of bounded model-checking, we reconsider the problem of constructing models of discrete-time Duration Calculus formulae. While this problem is known to be non-elementary when arbitrary length models are considered [Hansen94], it turns out to be only NP-complete when constrained to bounded length. As a corollary we obtain that model construction is in NP for the formulae actually encountered in case studies using Duration Calculus, as these have a certain small-model property. First experiments with a prototype implementation of the procedures demonstrate a competitive performance
On the complexity of drawing trees nicely: corrigendum
No full textIn this journal, Supowit and Reingold have given a proof that it is NP-complete to decide whether a binary tree can be drawn on a grid with width 24 if certain aesthetic requirements are obeyed. We identify and repair a mistake in their proof
Ernst Weiss
No full textDigital ImageThe Austrian author Ernst Weiss was born in 1882 in Brno. He died 1940 in Paris
Correctness of concurrent processes
No full textA new notion of correctness for concurrent processes is introduced and investigated. It is a relationship P sat S between process terms P built up from operators of CCS [Mi 80], CSP [Ho 85] and COSY [LTS 79] and logical formulas S specifying sets of finite communication sequences as in [Zw 89]. The definition of P sat S is based on a Petri net semantics for process terms [Ol 89]. The main point is that P sat S requires a simple liveness property of the net denoted by P. This implies that P is divergence free and externally deterministic.
Process correctness P sat S determines a new semantic model for process terms and logical formulas. It is a modification ℜ* of the readiness semantics [OH 86] which is fully abstract with respect to the relation P sat S. The model ℜ* abstracts from the concurrent behaviour of process terms and certain aspects of their internal activity. In ℜ* process correctness P sat S boils down to semantic equality: ℜ*[P]=ℜ*[S]. The modified readiness equivalence is closely related to failure equivalence [BHR 84] and strong testing equivalence [DH 84]
- …
