Philippe Darondeau

I&C Journal 2010 Journal Article

Quasi-static scheduling of communicating tasks

• Philippe Darondeau
• Blaise Genest
• P.S. Thiagarajan
• Shaofa Yang

Good scheduling policies for distributed embedded applications are required for meeting hard real time constraints and for optimizing the use of computational resources. We study the quasi-static scheduling problem in which (uncontrollable) control flow branchings can influence scheduling decisions at run time. Our abstracted distributed task model consists of a network of sequential processes that communicate via point-to-point buffers. In each round, the task gets activated by a request from the environment. When the task has finished computing the required responses, it reaches a pre-determined configuration and is ready to receive a new request from the environment. For such systems, we prove that determining the existence of a scheduling policy that guarantees upper bounds on buffer capacities is undecidable. However, we show that the problem is decidable for the important subclass of “data-branching” systems in which control flow branchings are exclusively due to data-dependent internal choices made by the sequential components. This decidability result exploits ideas derived from the Karp and Miller coverability tree for Petri nets as well as the existential boundedness notion of languages of message sequence charts.

TCS Journal 2005 Journal Article

Transition systems without transitions

• Andrzej M. Borzyszkowski
• Philippe Darondeau

We study the problem of embedding partial 2-structures into set 2-structures such that the target structure is full and forward closed and it is minimal w. r. t. these properties. Ehrenfeucht and Rozenberg introduced the notion of partial 2-structures—an abstract form of transition systems—and studied the problem of representing them as partial set 2-structures—directed graphs made of sets and their ordered symmetric differences. They constructed a representation and gave the conditions under which the representation is an isomorphism. We propose an alternative representation of partial 2-structures by partial set 2-structures which are complete graphs, hence their transitions may be left implicit, yielding a static representation of dynamic systems.

TCS Journal 2001 Journal Article

On the Petri net realization of context-free graphs

• Philippe Darondeau

Given a finite or infinite labeled transition graph defined by a graph grammar, we show an algorithm that decides whether this graph is isomorphic to the reachable state graph of some finite unlabeled Petri net and that produces in this case a minimal net realizing the graph.

I&C Journal 1999 Journal Article

Context-Free Event Domains Are Recognizable

• Eric Badouel
• Philippe Darondeau
• Jean-Claude Raoult

The possibly non-distributive event domains which arise from Winskel's event structures with binary conflict are known to coincide with the domains of configurations of Stark's trace automata. We prove that whenever the transitive reduction of the order on finite elements in an event domain is a context-free graph in the sense of Müller and Schupp, the event domain may also be generated from a finite trace automaton, where both the set of states and the concurrent alphabet are finite. We show that the set of graph grammars which generate event domains is a recursive set. We obtain altogether an effective procedure which decides from an unlabeled graph grammar whether it generates an event domain and which constructs in that case a finite trace automaton recognizing that event domain.

TCS Journal 1997 Journal Article

The synthesis problem for elementary net systems is NP-complete

• Eric Badouel
• Luca Bernardinello
• Philippe Darondeau

Given a labelled graph representing the sequential behaviour of some system, the synthesis problem consists in deciding whether it is the behaviour of a Petri net. This problem was solved by Ehrenfeucht and Rozenberg for the class of elementary net systems, relying on regions in graphs introduced as sets of nodes liable to represent extensions of places of a net. The solution was extended later on to pure place/transition nets using a variant notion of generalized regions. The naive method of synthesis which relies on this principle leads to exponential algorithms for an arbitrary class of nets. In an earlier study, we gave an algorithm that solves the synthesis problem in polynomial time for the class of pure place/transition nets. We show here that in contrast the synthesis problem is indeed NP-complete for the class of elementary nets.

TCS Journal 1993 Journal Article

Refinement of actions in event structures and causal trees

• Philippe Darondeau
• Pierpaolo Degano

Refinement of actions allows one to design systems in a top-down style, changing the level of abstraction by interpreting actions on a higher level by more complicated processes on a lower level. We study action refinement in two connected models for true concurrency. The first model is an adaptation of prime event structures, called δ-free event structures. In this model refinement amounts to an expansion of events into event structures. Refinement is compatible with the history-preserving equivalence on event structures. The second model, called causal trees, is an explicit representation for event structures factored by history-preserving bisimulation. Causal trees are equipped with derived refinement operations, defined in an inductive way. The two models for refinement are shown to agree. Causal trees may, therefore, be used to construct a semantic calculus for algebras of process terms enriched with refinement, where terms are interpreted as classes of history-preserving equivalent event structures.

TCS Journal 1992 Journal Article

Fairness, distances and degrees

• Philippe Darondeau
• Doris Nolte
• Lutz Priese
• Serge Yoccoz

We show the identity between sets of fair computations in recursive transition graphs, sets of cluster points of finite computations for Π0 1 ultra-metrics refining the Baire metrics, and Π0 3 subsets of ωω. The results are applied to recursive marked trees, fairness definitions, ω-regular languages, and Π0 3 sets.

I&C Journal 1992 Journal Article

Proof systems for infinite behaviours

• Philippe Darondeau
• Serge Yoccoz

We introduce several generalizations of testing to ω-behaviours of communicating processes, analyse the logical complexity of the testing equivalences, and establish on that basis a connection with proof systems.

TCS Journal 1991 Journal Article

On guarded recursion

• Eric Badouel
• Philippe Darondeau

We introduce a logical notion of well-guardedness for recursive terms on arbitrary signatures defined in Plotkin's framework of structural operational specifications, restricted by se Simone's realizability requirements. We then suggest a simpler form for the logical rule that gives the behaviour of a recursively defined expression in terms of the behaviour of its unfoldings. For well-guarded terms, the simplified rule is logically equivalent to the general rule, but it does not have the drawback of asking for premises more complex than consequences.

MFCS Conference 1990 Conference Paper

Event Structures, Causal Trees, and Refinements

• Philippe Darondeau
• Pierpaolo Degano

TCS Journal 1985 Journal Article

About fair asynchrony

• Philippe Darondeau

This paper examines the joint influence of fairness and asynchrony on the semantic modelling of a C. C. S. -like language. Fairness is the guarantee for every agent engaged in a computation to communicate with the other asynchronous agents if such communications are infinitely often possible. Programs are compared according to an implementation preorder which reflects the inclusion of observable properties: whenever, for every context |c and for every program r, no computation of r, experimenting upon |c (p) allows to recognize p versus q, p is considered less than q. A fully abstract model of the preorder is constructed in a domain of infinitary language, preferred here to classical algebraic domains. The restriction to bounded parallelism is analysed. In that simplified framework, the model turns effective and, moreover, decidable.