Igor Walukiewicz - CNRS, LaBRI, université de Bordeaux

Igor Walukiewicz
Are you Igor Walukiewicz?

Claim your profile, edit publications, add additional information:

Contact Details

Name
Igor Walukiewicz
Affiliation
CNRS, LaBRI, université de Bordeaux
City
Bordeaux
Country
France

Pubs By Year

Pub Categories

 
Computer Science - Logic in Computer Science (19)
 
Computer Science - Computer Science and Game Theory (3)

Publications Authored By Igor Walukiewicz

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. Read 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. Read 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. Read More

We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSOL) is well suited to express properties of such trees. We give a type system for ensuring that the result of the execution of a lambda-Y-program satisfies a given wMSOL property. Read 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. Read More

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. Read More

We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. Read 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. Read More

2015Mar
Affiliations: 1INRIA, LaBRI, université de Bordeaux, 2CNRS, LaBRI, université de Bordeaux

We propose a model-based approach to the model checking problem for recursive schemes. Since simply typed lambda calculus with the fixpoint operator, lambda-Y-calculus, is equivalent to schemes, we propose the use of a model of lambda-Y-calculus to discriminate the terms that satisfy a given property. If a model is finite in every type, this gives a decision procedure. Read More

We propose a new efficient algorithm for detecting if a cycle in a timed automaton can be iterated infinitely often. Existing methods for this problem have a complexity which is exponential in the number of clocks. Our method is polynomial: it essentially does a logarithmic number of zone canonicalizations. Read More

The distributed synthesis problem is about constructing cor- rect distributed systems, i.e., systems that satisfy a given specification. Read More

We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. Read More

We use the recently developed theory of forest algebras to find algebraic characterizations of the languages of unranked trees and forests definable in various logics. These include the temporal logics CTL and EF, and first-order logic over the ancestor relation. While the characterizations are in general non-effective, we are able to use them to formulate necessary conditions for definability and provide new proofs that a number of languages are not definable in these logics. Read More

2012Aug

Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for these automata is decidable. This result implies new decidability results for fragments of timed temporal logics. Read More

2012Mar
Affiliations: 1INRIA - IRISA, 2LaBRI, 3LaBRI, 4LaBRI
Category:

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. Read More

The reachability problem for timed automata asks if there exists a path from an initial state to a target state. The standard solution to this problem involves computing the zone graph of the automaton, which in principle could be infinite. In order to make the graph finite, zones are approximated using an extrapolation operator. Read More

We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. These abstractions preserve underlying simulation relations on the state space of the automaton. Read More

The B\"uchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the B\"uchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, it is shown that this simple transformation may sometimes result in an exponential blowup. Read 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. Read More

We prove an n-EXPTIME lower bound for the problem of deciding the winner in a reachability game on Higher Order Pushdown Automata (HPDA) of level n. This bound matches the known upper bound for parity games on HPDA. As a consequence the mu-calculus model checking over graphs given by n-HPDA is n-EXPTIME complete. Read More

We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy. Read More

We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy. Read More

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages which is closed under boolean operations and which has an effective presentation. Read More