1,721,140 research outputs found
Front Matter, Table of Contents, Preface, Organization, List of Authors
No full textFront Matter, Table of Contents, Preface, Organization, List of Author
Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
Full text linkVerification of concurrent systems is a difficult problem in general, and this is the case even more in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague proposed an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory for which safety properties can be effectively verified. All processes in Hague's setting are pushdown automata. Here, we extend it by considering other formal models and, as a main contribution, find very liberal conditions on the individual processes under which the safety problem is decidable: the only substantial condition we require is the effective computability of the downward closure for the class of the leader processes. Furthermore, our result allows for a hierarchical approach to constructing models of concurrent systems with decidable safety problem: networks with tree-like architecture, where each process shares a register with its children processes (and another register with its parent). Nodes in such networks can be for instance pushdown automata, Petri nets, or multi-pushdown systems with decidable reachability problem
Classifications of Recognizable Infinitary Trace Languages and the Distributed Synthesis Problem
No full textThe classification of recognizable ω-word languages into Borel levels is the basis of many specialized solutions in the fields of formal verification and algorithmic controller synthesis. Each of these levels is characterized by a class of deterministic ω-automata, namely deterministic weak (reachability and safety), deterministic Büchi, and deterministic Muller automata. This thesis analyses the more general setting of infinitary Mazurkiewicz traces, which model nonterminating, concurrent computation of distributed systems. The study of finitary trace-languages generalizes that of word-languages, and numerous results have been extended to infinitary trace-languages (due to Gastin, Petit, Diekert, Muscholl, and others). However, the current definitions of asynchronous ω-automata fail to yield a classification of ω-trace languages that is compatible with the Borel hierarchy. We close this gap, which had been open since the 1990's, by introducing the family of "synchronization aware'' automata. We also demonstrate the semi-decidability of the problem to determine whether a given recognizable ω-trace language is also recognized by a deterministic synchronization aware Büchi automaton.Although asynchronous automata are useful in implementing distributed monitors and distributed controllers, their constructions are prohibitively expensive even by automata-theoretic standards. On the other hand, "linearizations'' of infinitary trace languages, which invoke the framework of "trace-closed'' ω-word languages, can find immediate applications in model checking and formal verification of distributed systems. This is because word automata recognizing trace-closed languages support more efficient analyses of most of the interesting properties pertaining to distributed computations. In this setting, we present another classification of ω-trace languages in terms of a Borel-like hierarchy of trace-closed ω-word languages.Finally, we introduce a distributed version of Church's synthesis problem and compare it with two well known variants of distributed controller synthesis, viz. action-based control (due to Gastin, Lerman, and Zeitoun) and process-based control (due to Madhusudan, Thiagarajan, and Yang). While the algorithmic solution of these problems remains an open area of investigation, we build upon the work of Muscholl, Walukiewicz, and Zeitoun, and compare their problem classes with variants of distributed Church's synthesis problem by demonstrating suitable reductions in the sense that a solution of any one problem can be converted into a solution of the other
Vers la vérification de propriétés de sûreté pour des systèmes infinis communicants : décidabilité et raffinement des abstractions
No full textLa vérification de propriétés de sûreté des logiciels distribués basés sur des canaux fifo non bornés et fiables mène directement au model checking de systèmes infinis. Nous introduisons la famille des (q)ueueing (c)oncurrent (p)rocesses (QCP) composant des systèmes de transitions locaux, par exemple des automates finis/à pile, qui communiquent entre eux par des files fifo. Le problème d'atteignabilité des états de contrôle est indécidable pour des automates communicants et des automates à plusieurs piles, et par conséquent pour QCP.Nous présentons deux solutions pour contourner ce résultat négatif :Primo, une sur-approximation basée sur l'approche abstraire-tester-raffiner qui s'appuie sur notre nouveau concept de raffinement par chemin. Cette approche mène à permettre d'écrire un semi-algorithme du type CEGAR qui est implémenté avec des QDD et réalisé dans le framework McScM dont le banc d'essai conclut notre présentation.Secundo, nous proposons des restrictions pour les QCP à des piles locales pour démêler l'interaction causale entre les données locales (la pile), et la synchronisation globale. Nous montrons qu'en supposant qu'il existe une borne existentielle sur les exécutions et qu'en ajoutant une condition sur l'architecture, qui entrave la synchronisation de deux piles, on arrive à une réponse positive pour le problème de décidabilité de l'atteignabilité qui est EXPTime-complet (et qui généralise des résultats déjà connus). La construction de base repose sur une simulation du système par un automate à une pile équivalent du point de vue de l'atteignabilité --- sous-jacente, nos deux restrictions restreignent les exécutions à une forme hors-contexte. Nous montrons aussi que ces contraintes apparaissent souvent dans des situations ``concrètes''et qu'elles sont moins restrictives que celles actuellement connues. Une autre possibilité pour arriver à une solution pratiquement utilisable consiste à supposer une borne du problème de décidabilité : nous montrons que l'atteignabilité par un nombre borné de phases est décidable par un algorithme constructif qui est 2EXPTime-complet.Finalement, nous montrons qu'élargir les résultats positifs ci-dessus à la vérification de la logique linéaire temporelle demande soit de sacrifier l'expressivité de la logique soit d'ajouter des restrictions assez fortes aux QCP --- deux restrictions qui rendent cette approche inutilisable en pratique. En réutilisant notre argument de type ``hors-contexte'', nous représentons l'ordre partiel sous-jacent aux exécutions par des grammaires hypergraphes. Cela nous permet de bénéficier de résultats connus concertant le model checking des formules de la logique MSO sur les graphes (avec largeur arborescente bornée), et d'arriver aux premiers résultats concernant la vérification des propriétés sur l'ordre partiel des automates (à pile) communicants.The safety verification of distributed programs, that are based on reliable, unbounded fifo communication, leads in a straight line to model checking of infinite state systems. We introduce the family of (q)ueueing (c)oncurrent (p)rocesses (QCP): local transition systems, e.g., (pushdown-)automata, that are globally communicating over fifo channels. QCP inherits thus the known negative answers to the control-state reachability question from its members, above all from communicating automata and multi-stack pushdown systems. A feasible resolution of this question is, however, the corner stone for safety verification.We present two solutions to this intricacy: first, an over-approximation in the form of an abstract-check-refine algorithm on top of our novel notion of path invariant based refinement. This leads to a \cegar semi-algorithm that is implemented with the help of QDD and realized in a small software framework (McScM); the latter is benchmarked on a series ofsmall example protocols. Second, we propose restrictions for QCP with local pushdowns that untangle the causal interaction of local data, i.e., thestack, and global synchronization. We prove that an existential boundedness condition on runs together with an architectural restriction, that impedes the synchronization of two pushdowns, is sufficient and leads to an EXPTime-complete decision procedure (thus subsuming and generalizing known results). The underlying construction relies on a control-state reachability equivalent simulation on a single pushdown automaton, i.e., the context-freeness of the runs under the previous restrictions. We can demonstrate that our constraints arise ``naturally'' in certain classes of practical situations and are less restrictive than currently known ones. Another possibility to gain a practicable solution to safety verification involves limiting the decision question itself: we show that bounded phase reachability is decidable by a constructive algorithms in 2ExpTime, which is complete.Finally, trying to directly extend the previous positive results to model checking of linear temporal logic is not possible withouteither sacrificing expressivity or adding strong restrictions (i.e., that are not usable in practice). However, we can lift our context-freeness argument via hyperedge replacement grammars to graph-like representation of the partial order underlying each run of a QCP. Thus, we can directly apply the well-known results on MSO model checking on graphs (of bounded treewidth) to our setting and derive first results on verifying partial order properties on communicating (pushdown-) automata
Classifications of Recognizable Infinitary Trace Languages and the Distributed Synthesis Problem
No full textThe classification of recognizable ω-word languages into Borel levels is the basis of many specialized solutions in the fields of formal verification and algorithmic controller synthesis. Each of these levels is characterized by a class of deterministic ω-automata, namely deterministic weak (reachability and safety), deterministic Büchi, and deterministic Muller automata. This thesis analyses the more general setting of infinitary Mazurkiewicz traces, which model nonterminating, concurrent computation of distributed systems. The study of finitary trace-languages generalizes that of word-languages, and numerous results have been extended to infinitary trace-languages (due to Gastin, Petit, Diekert, Muscholl, and others). However, the current definitions of asynchronous ω-automata fail to yield a classification of ω-trace languages that is compatible with the Borel hierarchy. We close this gap, which had been open since the 1990's, by introducing the family of "synchronization aware'' automata. We also demonstrate the semi-decidability of the problem to determine whether a given recognizable ω-trace language is also recognized by a deterministic synchronization aware Büchi automaton.Although asynchronous automata are useful in implementing distributed monitors and distributed controllers, their constructions are prohibitively expensive even by automata-theoretic standards. On the other hand, "linearizations'' of infinitary trace languages, which invoke the framework of "trace-closed'' ω-word languages, can find immediate applications in model checking and formal verification of distributed systems. This is because word automata recognizing trace-closed languages support more efficient analyses of most of the interesting properties pertaining to distributed computations. In this setting, we present another classification of ω-trace languages in terms of a Borel-like hierarchy of trace-closed ω-word languages.Finally, we introduce a distributed version of Church's synthesis problem and compare it with two well known variants of distributed controller synthesis, viz. action-based control (due to Gastin, Lerman, and Zeitoun) and process-based control (due to Madhusudan, Thiagarajan, and Yang). While the algorithmic solution of these problems remains an open area of investigation, we build upon the work of Muscholl, Walukiewicz, and Zeitoun, and compare their problem classes with variants of distributed Church's synthesis problem by demonstrating suitable reductions in the sense that a solution of any one problem can be converted into a solution of the other
Lessons in Software Evolution Learned by Listening to Smalltalk
Full text linkThe biggest challenge facing software developers today is how to gracefully evolve complex software systems in the face of changing requirements. We clearly need software systems to be more dynamic, compositional and model-centric, but instead we continue to build systems that are static, baroque and inflexible. How can we better build change-enabled systems in the future? To answer this question, we propose to look back to one of the most successful systems to support change, namely Smalltalk. We briefly introduce Smalltalk with a few simple examples, and draw some lessons for software evolution. Smalltalk's simplicity, its reflective design, and its highly dynamic nature all go a long way towards enabling change in Smalltalk applications. We then illustrate how these lessons work in practice by reviewing a number of research projects that support software evolution by exploiting Smalltalk's design. We conclude by summarizing open issues and challenges for change-enabled systems of the future
Verification and synthesis of distributed systems with weak synchronisation
No full textLes programmes distribués sont une source de difficulté pour les méthodes formelles. Les interactions de plusieurs composantes provoquent une explosion combinatoire qui complexifie la vérification. Dans le cadre de la synthèse de contrôleurs, à cela s'ajoute le fait que les stratégies d'une composante ne peuvent tenir compte que d'une vision partielle du système. Ceci a mené à de nombreux résultats d'indécidabilité dans le domaine et des complexités très élevées dans les cas décidables. Dans cette thèse, nous proposons une approche permettant de décomposer les problèmes de vérification et de synthèse en instances locales aux processus. Cette approche mène à des résultats de décidabilité, et même dans certains cas à des algorithmes de complexités suffisamment basses pour envisager des applications. Nous montrons que cette méthode s'applique dans des systèmes distribués avec une communication restreinte entre les composantes: d'une part des systèmes où la communication se fait via la prise et le relâchement de locks, et d'autre part des systèmes où les processus communiquent par broadcast. De plus, nous utilisons cette approche dans des modèles a priori très différents, où le nombre de processus est constant, évolue dynamiquement, ou encore est paramétré.Distributed programs are a cause of difficulty for formal methods. The interactions of multiple components lead to a combinatorial explosion, which complicates verification. In the context of controller synthesis, this is further compounded by the fact that the strategies of one component can only take into account a partial view of the system. This has led to numerous undecidability results in the field and very high complexities in decidable cases. In this thesis, we propose an approach that allows the decomposition of verification and synthesis problems into local instances for individual processes. This approach leads to decidability results, and in some cases, to algorithms with low enough complexity to consider practical applications. We show that this method applies to distributed systems with restricted communication between components: on the one hand, systems where communication is limited to the acquisition and release of locks, and on the other hand, systems where processes communicate via broadcast. Moreover, we apply this approach to models that are quite different, where the number of processes is constant, evolves dynamically, or is parameterised
Verification of Automata with Storage Mechanisms
Full text linkAn important question in computer science is to ask, whether a given system conforms to a specification. Often this question is equivalent to ask whether a finite automaton with certain memory like a stack or queue can reach some given state. In this thesis we focus this reachability problem of automata having one or more lossy or reliable stacks or queues as their memory. Unfortunately, the reachability problem is undecidable or of high complexity in most of these cases. We circumvent this by several approximation methods. So we extend the exploration algorithm by Boigelot and Godefroid under-approximating the reachability problem of queue automata. We also study some automata having multiple stacks with a restricted behavior. These “asynchronous pushdown systems” have an efficiently decidable reachability problem. To show our results we first have to gain knowledge of several algebraic properties of the so-called transformation monoid of the studied storage mechanisms.An important research topic in computer science is the verification, i.e., the analysis of systems towards their correctness. This analysis consists of two parts: first we have to formalize the system and the desired properties. Afterwards we have to find algorithms to check whether the properties hold in the system. In many cases we can model the system as a finite automaton with a suitable storage mechanism, e.g., functional programs with recursive calls can be modeled as automata with a stack (or pushdown). Here, we consider automata with two variations of stacks and queues: 1. Partially lossy queues and stacks, which are allowed to forget some specified parts of their contents at any time. We are able to model unreliable systems with such memories. 2. Distributed queues and stacks, i.e., multiple such memories with a special synchronization in between. Often we can check the properties of our models by solving the reachability and recurrent reachability problems in our automata models. It is well-known that the decidability of these problems highly depends on the concrete data type of our automata’s memory. Both problems can be solved in polynomial time for automata with one stack. In contrast, these problems are undecidable if we attach a queue or at least two stacks to our automata. In some special cases we are still able to verify such systems. So, we will consider only special automata with multiple stacks - so-called asynchronous pushdown automata. These are multiple (local) automata each having one stack. Whenever these automata try to write something into at least one stack, we require a read action on these stacks right before these actions. We will see that the (recurrent) reachability problem is decidable for such asynchronous pushdown automata in polynomial time. We can also semi-decide the reachability problem of our queue automata by exploration of the configration space. To this end, we can join multiple consecutive transitions to so-called meta-transformations and simulate them at once. Here, we study meta-transformations alternating between writing words from a given regular language into the queues and reading words from another regular language from the queues. We will see that such metatransformations can be applied in polynomial time. To show this result we first study some algebraic properties of our stacks and queues.Ein wichtiges Forschungsthema in der Informatik ist die Verifikation, d.h., die Analyse von Systemen bezüglich ihrer Korrektheit. Diese Analyse erfolgt in zwei Schritten: Zuerst müssen wir das System und die gewünschten Eigenschaften formalisieren. Anschließend benötigen wir Algorithmen zum Testen, ob das System die Eigenschaften erfüllt. Oftmals können wir das Systemals endlichen Automaten mit geeignetem Speichermechanismus modellieren, z.B. rekursive Programme sind im Wesentlichen Automaten mit einem Stack. Hier betrachten wir Automaten mit zwei Varianten von Stacks und Queues: 1. Partiell vergessliche Stacks und Queues, welche bestimmte Teile ihrer Inhalte jederzeit vergessen können. Diese können für unzuverlässige Systeme verwendet werden. 2. Verteilte Stacks und Queues, d.h., mehrere Stacks und Queues mit vordefinierter Synchronisierung. Häufig lassen sich die Eigenschaften unserer Modelle mithilfe des (wiederholten) Erreichbarkeitsproblems in unseren Automaten lösen. Dabei ist bekannt, dass die Entscheidbarkeit dieser Probleme oftmals stark vom konkreten Datentyp des Speichers abhängt. Beide Probleme können für Automaten mit einem Stack in Polynomialzeit gelöst werden. Sie sind jedoch unentscheidbar, wenn wir Automaten mit einer Queue oder zwei Stacks betrachten. In bestimmten Spezialfällen sind aber dennoch in der Lage diese Systeme zu verifizieren. So können wir beispielsweise bestimmte Automaten mit mehreren Stacks betrachten - so genannte Asynchrone Kellerautomaten. Diese bestehen aus mehreren (lokalen) Automaten mit jeweils einem Stack. Wann immer diese Automaten etwas in mind. einen Stack schreiben, müssen sie unmittelbar zuvor von diesen Stacks etwas lesen. Das (wiederholte) Erreichbarkeitsproblem ist in asynchronen Kellerautomaten in Polynomialzeit entscheidbar. Wir können zudem das Erreichbarkeitsproblem von Queueautomaten durch Exploration des Konfigurationsraums semi-entscheiden. Hierzu können wir mehrere aufeinanderfolgende Transitionen zu so genannten Meta-Transformationen zusammenfassen und diese in einem Schritt simulieren. Hier betrachten wir Meta-Transformationen, die zwischen dem Lesen und Schreiben von Wörtern aus zwei gegebenen regulären Sprachen alternieren. Diese Meta-Transformationen können in Polynomialzeit ausgeführt werden. Für dieses Ergebnis müssen wir jedoch zunächst verschiedene algebraische Eigenschaften der Queues betrachten
On the complementation of asynchronous cellular Büchi automata
No full textAbstractWe present direct subset automata constructions for asynchronous (asynchronous cellular, resp.) automata. This provides a solution to the problem of direct determinization for automata with distributed control for languages of finite traces. We use the subset automaton construction and apply Klarlund's progress measure technique in order to complement non-deterministic asynchronous cellular Büchi automata for infinite traces. Both constructions yield a super-exponential blow-up in the size of local states sets
- …
