-
An automata-based approach for synchronizable mailbox communication
Authors:
Romain Delpy,
Anca Muscholl,
Grégoire Sutre
Abstract:
We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sen…
▽ More
We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is Pspace-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (Pspace) of several questions considered in previous literature.
△ Less
Submitted 19 December, 2024; v1 submitted 9 July, 2024;
originally announced July 2024.
-
Finite-valued Streaming String Transducers
Authors:
Emmanuel Filiot,
Ismaël Jecker,
Christof Löding,
Anca Muscholl,
Gabriele Puppis,
Sarah Winter
Abstract:
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finite-valued transducers very attractive. For classical transducers, it is also known that fini…
▽ More
A transducer is finite-valued if for some bound k, it maps any given input to at most k outputs. For classical, one-way transducers, it is known since the 80s that finite valuedness entails decidability of the equivalence problem. This decidability result is in contrast to the general case, which makes finite-valued transducers very attractive. For classical transducers, it is also known that finite valuedness is decidable and that any k-valued finite transducer can be decomposed as a union of k single-valued finite transducers.
In this paper, we extend the above results to copyless streaming string transducers (SSTs), answering questions raised by Alur and Deshmukh in 2011. SSTs strictly extend the expressiveness of one-way transducers via additional variables that store partial outputs. We prove that any k-valued SST can be effectively decomposed as a union of k (single-valued) deterministic SSTs. As a corollary, we obtain equivalence of SSTs and two-way transducers in the finite-valued case (those two models are incomparable in general). Another corollary is an elementary upper bound for checking equivalence of finite-valued SSTs. The latter problem was already known to be decidable, but the proof complexity was unknown (it relied on Ehrenfeucht's conjecture). Finally, our main result is that finite valuedness of SSTs is decidable. The complexity is PSpace, and even PTime when the number of variables is fixed.
△ Less
Submitted 12 May, 2025; v1 submitted 13 May, 2024;
originally announced May 2024.
-
Model-checking parametric lock-sharing systems against regular constraints
Authors:
Corto Mascle,
Anca Muscholl,
Igor Walukiewicz
Abstract:
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verificat…
▽ More
In parametric lock-sharing systems processes can spawn new processes to run in parallel, and can create new locks. The behavior of every process is given by a pushdown automaton. We consider infinite behaviors of such systems under strong process fairness condition. A result of a potentially infinite execution of a system is a limit configuration, that is a potentially infinite tree. The verification problem is to determine if a given system has a limit configuration satisfying a given regular property. This formulation of the problem encompasses verification of reachability as well as of many liveness properties. We show that this verification problem, while undecidable in general, is decidable for nested lock usage. We show Exptime-completeness of the verification problem. The main source of complexity is the number of parameters in the spawn operation. If the number of parameters is bounded, our algorithm works in Ptime for properties expressed by parity automata with a fixed number of ranks.
△ Less
Submitted 10 July, 2023;
originally announced July 2023.
-
Distributed controller synthesis for deadlock avoidance
Authors:
Hugo Gimbert,
Corto Mascle,
Anca Muscholl,
Igor Walukiewicz
Abstract:
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two loc…
▽ More
We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes $Σ_2^P$-complete, and even in PTIME under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is NEXPTIME-complete. The drinking philosophers problem falls in this case.
△ Less
Submitted 17 June, 2025; v1 submitted 26 April, 2022;
originally announced April 2022.
-
Active Learning for Sound Negotiations
Authors:
Anca Muscholl,
Igor Walukiewicz
Abstract:
We present two active learning algorithms for sound deterministic negotiations. Sound deterministic negotiations are models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that this additional structure allows to minimize such negotiations. The two active learning algorithms differ in the type of membership queries they use. Both have similar co…
▽ More
We present two active learning algorithms for sound deterministic negotiations. Sound deterministic negotiations are models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that this additional structure allows to minimize such negotiations. The two active learning algorithms differ in the type of membership queries they use. Both have similar complexity to Angluin's L* algorithm, in particular, the number of queries is polynomial in the size of the negotiation, and not in the number of configurations.
△ Less
Submitted 6 May, 2022; v1 submitted 6 October, 2021;
originally announced October 2021.
-
One-way resynchronizability of word transducers
Authors:
Sougata Bose,
S. N. Krishna,
Anca Muscholl,
Gabriele Puppis
Abstract:
The origin semantics for transducers was proposed in 2014, and led to various characterizations and decidability results that are in contrast with the classical semantics. In this paper we add a further decidability result for characterizing transducers that are close to one-way transducers in the origin semantics. We show that it is decidable whether a non-deterministic two-way word transducer ca…
▽ More
The origin semantics for transducers was proposed in 2014, and led to various characterizations and decidability results that are in contrast with the classical semantics. In this paper we add a further decidability result for characterizing transducers that are close to one-way transducers in the origin semantics. We show that it is decidable whether a non-deterministic two-way word transducer can be resynchronized by a bounded, regular resynchronizer into an origin-equivalent one-way transducer. The result is in contrast with the usual semantics, where it is undecidable to know if a non-deterministic two-way transducer is equivalent to some one-way transducer.
△ Less
Submitted 20 January, 2021;
originally announced January 2021.
-
Pumping lemmas for weighted automata
Authors:
Agnishom Chattopadhyay,
Filip Mazowiecki,
Anca Muscholl,
Cristian Riveros
Abstract:
We present pumping lemmas for five classes of functions definable by fragments of weighted automata over the min-plus semiring, the max-plus semiring and the semiring of natural numbers. As a corollary we show that the hierarchy of functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous weighted automata, and the full class of weighted automata is strict for the min-plus and…
▽ More
We present pumping lemmas for five classes of functions definable by fragments of weighted automata over the min-plus semiring, the max-plus semiring and the semiring of natural numbers. As a corollary we show that the hierarchy of functions definable by unambiguous, finitely-ambiguous, polynomially-ambiguous weighted automata, and the full class of weighted automata is strict for the min-plus and max-plus semirings.
△ Less
Submitted 20 July, 2021; v1 submitted 17 January, 2020;
originally announced January 2020.
-
Minimization of visibly pushdown automata is NP-complete
Authors:
Olivier Gauwin,
Anca Muscholl,
Michael Raskin
Abstract:
We show that the minimization of visibly pushdown automata is NP-complete. This result is obtained by introducing immersions, that recognize multiple languages (over a usual, non-visible alphabet) using a common deterministic transition graph, such that each language is associated with an initial state and a set of final states. We show that minimizing immersions is NP-complete, and reduce this pr…
▽ More
We show that the minimization of visibly pushdown automata is NP-complete. This result is obtained by introducing immersions, that recognize multiple languages (over a usual, non-visible alphabet) using a common deterministic transition graph, such that each language is associated with an initial state and a set of final states. We show that minimizing immersions is NP-complete, and reduce this problem to the minimization of visibly pushdown automata.
△ Less
Submitted 12 February, 2020; v1 submitted 22 July, 2019;
originally announced July 2019.
-
On Synthesis of Resynchronizers for Transducers
Authors:
Sougata Bose,
Shankara Narayanan Krishna,
Anca Muscholl,
Vincent Penelle,
Gabriele Puppis
Abstract:
We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T1, T2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T1 is contained in R(T2) under the origin s…
▽ More
We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T1, T2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T1 is contained in R(T2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open.
△ Less
Submitted 24 June, 2019; v1 submitted 20 June, 2019;
originally announced June 2019.
-
Equivalence of finite-valued streaming string transducers is decidable
Authors:
Anca Muscholl,
Gabriele Puppis
Abstract:
In this paper we provide a positive answer to a question left open by Alur and and Deshmukh in 2011 by showing that equivalence of finite-valued copyless streaming string transducers is decidable.
In this paper we provide a positive answer to a question left open by Alur and and Deshmukh in 2011 by showing that equivalence of finite-valued copyless streaming string transducers is decidable.
△ Less
Submitted 30 April, 2019; v1 submitted 19 February, 2019;
originally announced February 2019.
-
Origin-equivalence of two-way word transducers is in PSPACE
Authors:
Sougata Bose,
Anca Muscholl,
Vincent Penelle,
Gabriele Puppis
Abstract:
We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered by adopting a slightly different, but natural semantics, call…
▽ More
We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered by adopting a slightly different, but natural semantics, called origin semantics and introduced by Bojanczyk in 2014. Specifically, we prove that the equivalence and containment problems for two-way word transducers in the origin semantics are PSPACE-complete. We also consider a variant of the containment problem where two-way transducers are compared under the origin semantics, but in a more relaxed way, by allowing distortions of the origins. The possible distortions are described by means of a resynchronization relation. We propose a logical formalism for describing a broad class of resynchronizations, while preserving the decidability of the variant of the containment problem.
△ Less
Submitted 5 October, 2018; v1 submitted 20 July, 2018;
originally announced July 2018.
-
One-way definability of two-way word transducers
Authors:
Félix Baschenis,
Olivier Gauwin,
Anca Muscholl,
Gabriele Puppis
Abstract:
Functional transductions realized by two-way transducers (or, equally, by streaming transducers or MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown in 2013 that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different…
▽ More
Functional transductions realized by two-way transducers (or, equally, by streaming transducers or MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown in 2013 that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different flavor solving the above question, that has doubly exponential space complexity. In the special case of sweeping transducers the complexity is one exponential less. We also show how to construct an equivalent one-way transducer, whenever it exists, in doubly or triply exponential time, again depending on whether the input transducer is sweeping or two-way. In the sweeping case our construction is shown to be optimal.
△ Less
Submitted 6 December, 2018; v1 submitted 6 June, 2017;
originally announced June 2017.
-
Static Analysis of Deterministic Negotiations
Authors:
Javier Esparza,
Anca Muscholl,
Igor Walukiewicz
Abstract:
Negotiation diagrams are a model of concurrent computation akin to workflow Petri nets. Deterministic negotiation diagrams, equivalent to the much studied and used free-choice workflow Petri nets, are surprisingly amenable to verification. Soundness (a property close to deadlock-freedom) can be decided in PTIME. Further, other fundamental questions like computing summaries or the expected cost, ca…
▽ More
Negotiation diagrams are a model of concurrent computation akin to workflow Petri nets. Deterministic negotiation diagrams, equivalent to the much studied and used free-choice workflow Petri nets, are surprisingly amenable to verification. Soundness (a property close to deadlock-freedom) can be decided in PTIME. Further, other fundamental questions like computing summaries or the expected cost, can also be solved in PTIME for sound deterministic negotiation diagrams, while they are PSPACE-complete in the general case.
In this paper we generalize and explain these results. We extend the classical "meet-over-all-paths" (MOP) formulation of static analysis problems to our concurrent setting, and introduce Mazurkiewicz-invariant analysis problems, which encompass the questions above and new ones. We show that any Mazurkiewicz-invariant analysis problem can be solved in PTIME for sound deterministic negotiations whenever it is in PTIME for sequential flow-graphs---even though the flow-graph of a deterministic negotiation diagram can be exponentially larger than the diagram itself. This gives a common explanation to the low-complexity of all the analysis questions studied so far. Finally, we show that classical gen/kill analyses are also an instance of our framework, and obtain a PTIME algorithm for detecting anti-patterns in free-choice workflow Petri nets.
Our result is based on a novel decomposition theorem, of independent interest, showing that sound deterministic negotiation diagrams can be hierarchically decomposed into (possibly overlapping) smaller sound diagrams.
△ Less
Submitted 13 April, 2017;
originally announced April 2017.
-
Soundness in negotiations
Authors:
Javier Esparza,
Denis Kuperberg,
Anca Muscholl,
Igor Walukiewicz
Abstract:
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In earlier work, Esparza and Desel have shown that deciding soundness of a negotiatio…
▽ More
Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In earlier work, Esparza and Desel have shown that deciding soundness of a negotiation is Pspace-complete, and in Ptime if the negotiation is deterministic. They have also extended their polynomial soundness algorithm to an intermediate class of acyclic, non-deterministic negotiations. However, they did not analyze the runtime of the extended algorithm, and also left open the complexity of the soundness problem for the intermediate class. In the first part of this paper we revisit the soundness problem for deterministic negotiations, and show that it is Nlogspace-complete, improving on the earlier algorithm, which requires linear space. In the second part we answer the question left open by Esparza and Desel. We prove that the soundness problem can be solved in polynomial time for acyclic, weakly non- deterministic negotiations, a more general class than the one considered by them. In the third and final part, we show that the techniques developed in the first two parts of the paper can be applied to analysis problems other than soundness, including the problem of detecting race conditions, and several classical static analysis problems. More specifically, we show that, while these problems are intractable for arbitrary acyclic deterministic negotiations, they become tractable in the sound case. So soundness is not only a desirable behavioral property in itself, but also helps to analyze other properties.
△ Less
Submitted 15 January, 2018; v1 submitted 15 March, 2017;
originally announced March 2017.
-
Untwisting two-way transducers in elementary time
Authors:
Félix Baschenis,
Olivier Gauwin,
Anca Muscholl,
Gabriele Puppis
Abstract:
Functional transductions realized by two-way transducers (equivalently, by streaming transducers and by MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown recently (LICS'13) that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algori…
▽ More
Functional transductions realized by two-way transducers (equivalently, by streaming transducers and by MSO transductions) are the natural and standard notion of "regular" mappings from words to words. It was shown recently (LICS'13) that it is decidable if such a transduction can be implemented by some one-way transducer, but the given algorithm has non-elementary complexity. We provide an algorithm of different flavor solving the above question, that has double exponential space complexity. We further apply our technique to decide whether the transduction realized by a two-way transducer can be implemented by a sweeping transducer, with either known or unknown number of passes.
△ Less
Submitted 10 January, 2017;
originally announced January 2017.
-
Reachability for dynamic parametric processes
Authors:
Anca Muscholl,
Helmut Seidl,
Igor Walukiewicz
Abstract:
In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent.
We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems,…
▽ More
In a dynamic parametric process every subprocess may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent.
We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.
△ Less
Submitted 17 September, 2016;
originally announced September 2016.
-
On parametrized verification of asynchronous, shared-memory pushdown systems
Authors:
Marie Fortin,
Anca Muscholl,
Igor Walukiewicz
Abstract:
We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdar'13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar'15]. We show here that the liveness problem is PSPACE-complete. We also in…
▽ More
We consider the model of parametrized asynchronous shared-memory pushdown systems, as introduced in [Hague'11]. In a series of recent papers it has been shown that reachability in this model is PSPACE-complete [Esparza, Ganty, Majumdar'13] and that liveness is decidable in NEXPTIME [Durand-Gasselin, Esparza, Ganty, Majumdar'15]. We show here that the liveness problem is PSPACE-complete. We also introduce the universal reachability problem. We show that it is decidable, and coNEXPTIME-complete. Finally, using these results, we prove that the verifying regular properties of traces of executions, satisfying some stuttering condition, is also decidable in NEXPTIME for this model.
△ Less
Submitted 15 July, 2016; v1 submitted 28 June, 2016;
originally announced June 2016.
-
A Note on Monitors and Büchi automata
Authors:
Volker Diekert,
Anca Muscholl,
Igor Walukiewicz
Abstract:
When a property needs to be checked against an unknown or very complex system, classical exploration techniques like model-checking are not applicable anymore. Sometimes a~monitor can be used, that checks a given property on the underlying system at runtime. A monitor for a property $L$ is a deterministic finite automaton $M_L$ that after each finite execution tells whether (1) every possible exte…
▽ More
When a property needs to be checked against an unknown or very complex system, classical exploration techniques like model-checking are not applicable anymore. Sometimes a~monitor can be used, that checks a given property on the underlying system at runtime. A monitor for a property $L$ is a deterministic finite automaton $M_L$ that after each finite execution tells whether (1) every possible extension of the execution is in $L$, or (2) every possible extension is in the complement of $L$, or neither (1) nor (2) holds. Moreover, $L$ being monitorable means that it is always possible that in some future the monitor reaches (1) or (2). Classical examples for monitorable properties are safety and cosafety properties. On the other hand, deterministic liveness properties like "infinitely many $a$'s" are not monitorable. We discuss various monitor constructions with a focus on deterministic omega-regular languages. We locate a proper subclass of of deterministic omega-regular languages but also strictly large than the subclass of languages which are deterministic and codeterministic, and for this subclass there exists a canonical monitor which also accepts the language itself.
We also address the problem to decide monitorability in comparison with deciding liveness. The state of the art is as follows. Given a Büchi automaton, it is PSPACE-complete to decide liveness or monitorability. Given an LTL formula, deciding liveness becomes EXPSPACE-complete, but the complexity to decide monitorability remains open.
△ Less
Submitted 3 July, 2015;
originally announced July 2015.
-
Automated Synthesis of Distributed Controllers
Authors:
Anca Muscholl
Abstract:
Synthesis is a particularly challenging problem for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. This paper gives an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring. 1 Context Mo…
▽ More
Synthesis is a particularly challenging problem for concurrent programs. At the same time it is a very promising approach, since concurrent programs are difficult to get right, or to analyze with traditional verification techniques. This paper gives an introduction to distributed synthesis in the setting of Mazurkiewicz traces, and its applications to decentralized runtime monitoring. 1 Context Modern computing systems are increasingly distributed and heterogeneous. Software needs to be able to exploit these advances, providing means for applications to be more performant. Traditional concurrent programming paradigms, as in Java, are based on threads, shared-memory, and locking mechanisms that guard access to common data. More recent paradigms like the reactive programming model of Erlang [4] and Scala [35,36] replace shared memory by asynchronous message passing, where sending a message is non-blocking. In all these concurrent frameworks, writing reliable software is a serious challenge. Programmers tend to think about code mostly in a sequential way, and it is hard to grasp all possible schedulings of events in a concurrent execution. For similar reasons, verification and analysis of concurrent programs is a difficult task. Testing, which is still the main method for error detection in software, has low coverage for concurrent programs. The reason is that bugs in such programs are difficult to reproduce: they may happen under very specific thread schedules and the likelihood of taking such corner-case schedules is very low. Automated verification, such as model-checking and other traditional exploration techniques, can handle very limited instances of concurrent programs, mostly because of the very large number of possible states and of possible interleavings of executions. Formal analysis of programs requires as a prerequisite a clean mathematical model for programs. Verification of sequential programs starts usually with an abstraction step -- reducing the value domains of variables to finite domains, viewing conditional branching as non-determinism, etc. Another major simplification consists in disallowing recursion. This leads to a very robust computational model, namely finite-state automata and regular languages. Regular languages of words (and trees) are particularly well understood notions. The deep connections between logic and automata revealed by the foundational work of Büchi, Rabin, and others, are the main ingredients in automata-based verification .
△ Less
Submitted 8 June, 2015;
originally announced June 2015.
-
Distributed synthesis for acyclic architectures
Authors:
Anca Muscholl,
Igor Walukiewicz
Abstract:
The distributed synthesis problem is about constructing cor- rect distributed systems, i.e., systems that satisfy a given specification. We consider a slightly more general problem of distributed control, where the goal is to restrict the behavior of a given distributed system in order to satisfy the specification. Our systems are finite state machines that communicate via rendez-vous (Zielonka au…
▽ More
The distributed synthesis problem is about constructing cor- rect distributed systems, i.e., systems that satisfy a given specification. We consider a slightly more general problem of distributed control, where the goal is to restrict the behavior of a given distributed system in order to satisfy the specification. Our systems are finite state machines that communicate via rendez-vous (Zielonka automata). We show decidability of the synthesis problem for all omega-regular local specifications, under the restriction that the communication graph of the system is acyclic. This result extends a previous decidability result for a restricted form of local reachability specifications.
△ Less
Submitted 16 July, 2014; v1 submitted 13 February, 2014;
originally announced February 2014.
-
Reachability Analysis of Communicating Pushdown Systems
Authors:
Alexander Heussner,
Jérôme Leroux,
Anca Muscholl,
Grégoire Sutre
Abstract:
The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received). The problem is EXPTIME-compl…
▽ More
The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received). The problem is EXPTIME-complete in the decidable case. The second result is a doubly exponential time algorithm for bounded context analysis in this setting, together with a matching lower bound. Both results extend and improve previous work from La Torre et al.
△ Less
Submitted 28 September, 2012; v1 submitted 3 September, 2012;
originally announced September 2012.
-
On distributed monitoring of asynchronous systems
Authors:
Volker Diekert,
Anca Muscholl
Abstract:
Distributed systems are notoriously difficult to understand and analyze in order to assert their correction w.r.t. given properties. They often exhibit a huge number of different behaviors, as soon as the active entities (peers, agents, processes, etc) behave in an asynchronous manner. Already the modelization of such systems is a non-trivial task, let alone their formal verification.
The purpos…
▽ More
Distributed systems are notoriously difficult to understand and analyze in order to assert their correction w.r.t. given properties. They often exhibit a huge number of different behaviors, as soon as the active entities (peers, agents, processes, etc) behave in an asynchronous manner. Already the modelization of such systems is a non-trivial task, let alone their formal verification.
The purpose of this paper is to discuss the problem of distributed monitoring on a simple model of finite-state distributed automata based on shared actions, called asynchronous automata. Monitoring is a question related to runtime verification: assume that we have to check a property $L$ against an unknown or very complex system $A$, so that classical static analysis is not possible. Therefore instead of model-checking a monitor is used, that checks the property on the underlying system at runtime.
We are interested here in monitoring distributed systems modeled as asynchronous automata. It is natural to require that monitors should be of the same kind as the underlying system, so we consider here distributed monitoring. A distributed monitor does not have a global view of the system, therefore we propose the notion of locally monitorable trace language. Our main result shows that if the distributed alphabet of actions is connected and if $L$ is a set of infinite traces such that both $L$ and its complement $L^c$ are countable unions of locally safety languages, then $L$ is locally monitorable. We also show that over infinite traces, recognizable countable unions of locally safety languages are precisely the complements of deterministic languages.
△ Less
Submitted 10 August, 2012;
originally announced August 2012.
-
On Injective Embeddings of Tree Patterns
Authors:
Jakub Michaliszyn,
Anca Muscholl,
Sławek Staworko,
Piotr Wieczorek,
Zhilin Wu
Abstract:
We study three different kinds of embeddings of tree patterns: weakly-injective, ancestor-preserving, and lca-preserving. While each of them is often referred to as injective embedding, they form a proper hierarchy and their computational properties vary (from P to NP-complete). We present a thorough study of the complexity of the model checking problem i.e., is there an embedding of a given tree…
▽ More
We study three different kinds of embeddings of tree patterns: weakly-injective, ancestor-preserving, and lca-preserving. While each of them is often referred to as injective embedding, they form a proper hierarchy and their computational properties vary (from P to NP-complete). We present a thorough study of the complexity of the model checking problem i.e., is there an embedding of a given tree pattern in a given tree, and we investigate the impact of various restrictions imposed on the tree pattern: bound on the degree of a node, bound on the height, and type of allowed labels and edges.
△ Less
Submitted 28 April, 2012; v1 submitted 22 April, 2012;
originally announced April 2012.
-
Asynchronous Games over Tree Architectures
Authors:
Blaise Genest,
Hugo Gimbert,
Anca Muscholl,
Igor Walukiewicz
Abstract:
We consider the task of controlling in a distributed way a Zielonka asynchronous automaton. Every process of a controller has access to its causal past to determine the next set of actions it proposes to play. An action can be played only if every process controlling this action proposes to play it. We consider reachability objectives: every process should reach its set of final states. We show th…
▽ More
We consider the task of controlling in a distributed way a Zielonka asynchronous automaton. Every process of a controller has access to its causal past to determine the next set of actions it proposes to play. An action can be played only if every process controlling this action proposes to play it. We consider reachability objectives: every process should reach its set of final states. We show that this control problem is decidable for tree architectures, where every process can communicate with its parent, its children, and with the environment. The complexity of our algorithm is l-fold exponential with l being the height of the tree representing the architecture. We show that this is unavoidable by showing that even for three processes the problem is EXPTIME-complete, and that it is non-elementary in general.
△ Less
Submitted 15 February, 2013; v1 submitted 31 March, 2012;
originally announced April 2012.
-
Verifying Recursive Active Documents with Positive Data Tree Rewriting
Authors:
Blaise Genest,
Anca Muscholl,
Zhilin Wu
Abstract:
This paper proposes a data tree-rewriting framework for modeling evolving documents. The framework is close to Guarded Active XML, a platform used for handling XML repositories evolving through web services. We focus on automatic verification of properties of evolving documents that can contain data from an infinite domain. We establish the boundaries of decidability, and show that verification…
▽ More
This paper proposes a data tree-rewriting framework for modeling evolving documents. The framework is close to Guarded Active XML, a platform used for handling XML repositories evolving through web services. We focus on automatic verification of properties of evolving documents that can contain data from an infinite domain. We establish the boundaries of decidability, and show that verification of a {\em positive} fragment that can handle recursive service calls is decidable. We also consider bounded model-checking in our data tree-rewriting framework and show that it is $\nexptime$-complete.
△ Less
Submitted 4 March, 2010;
originally announced March 2010.
-
A lower bound on web services composition
Authors:
Anca Muscholl,
Igor Walukiewicz
Abstract:
A web service is modeled here as a finite state machine. A composition problem for web services is to decide if a given web service can be constructed from a given set of web services; where the construction is understood as a simulation of the specification by a fully asynchronous product of the given services. We show an EXPTIME-lower bound for this problem, thus matching the known upper bound…
▽ More
A web service is modeled here as a finite state machine. A composition problem for web services is to decide if a given web service can be constructed from a given set of web services; where the construction is understood as a simulation of the specification by a fully asynchronous product of the given services. We show an EXPTIME-lower bound for this problem, thus matching the known upper bound. Our result also applies to richer models of web services, such as the Roman model.
△ Less
Submitted 15 May, 2008; v1 submitted 18 April, 2008;
originally announced April 2008.
