Paul Gastin

TACAS Conference 2026 Conference Paper

TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics

• S Akshay
• Prerak Contractor
• Paul Gastin
• R Govind
• B Srivathsan

I&C Journal 2022 Journal Article

Regular transducer expressions for regular transformations

• Vrunda Dave
• Paul Gastin
• Shankara Narayanan Krishna

Functional MSO transductions, deterministic two-way transducers, as well as streaming string transducers are all equivalent models for regular functions. In this paper, we show that every regular function, either on finite words or on infinite words, captured by a deterministic two-way transducer, can be described with a regular transducer expression (RTE ). For infinite words, the two-way transducer uses Muller acceptance and ω-regular look-ahead. RTEs are constructed from constant functions using the combinators if-then-else (deterministic choice), Hadamard product, and unambiguous versions of the Cauchy product, the 2-chained Kleene-iteration and the 2-chained omega-iteration. Our proof works for transformations of both finite and infinite words, extending the result on finite words of Alur et al. in LICS'14. The construction of an RTE associated with a deterministic two-way transducer is guided by a regular expression which is “good” wrt. its transition monoid. “Good” expressions are unambiguous, ensuring the functionality of the output computed. Moreover, in “good” expressions, iterations (Kleene-plus or omega) are restricted to subexpressions corresponding to idempotent elements of the transition monoid. “Good” expressions can be obtained with an unambiguous version of Imre Simon's famous forest factorization theorem. To handle infinite words, we introduce the notion of transition monoids for deterministic two-way Muller transducers with look-ahead, where the look-ahead is captured by some backward deterministic Büchi automaton. This paper is an extended version of [15] presented at LICS'18.

MFCS Conference 2020 Conference Paper

Register Transducers Are Marble Transducers

• Gaëtan Douéneau-Tabot
• Emmanuel Filiot
• Paul Gastin

Deterministic two-way transducers define the class of regular functions from words to words. Alur and Cerný introduced an equivalent model of transducers with registers called copyless streaming string transducers. In this paper, we drop the "copyless" restriction on these machines and show that they are equivalent to two-way transducers enhanced with the ability to drop marks, named "marbles", on the input. We relate the maximal number of marbles used with the amount of register copies performed by the streaming string transducer. Finally, we show that the class membership problems associated with these models are decidable. Our results can be interpreted in terms of program optimization for simple recursive and iterative programs.

MFCS Conference 2019 Conference Paper

Aperiodic Weighted Automata and Weighted First-Order Logic

• Manfred Droste
• Paul Gastin

By fundamental results of Schützenberger, McNaughton and Papert from the 1970s, the classes of first-order definable and aperiodic languages coincide. Here, we extend this equivalence to a quantitative setting. For this, weighted automata form a general and widely studied model. We define a suitable notion of a weighted first-order logic. Then we show that this weighted first-order logic and aperiodic polynomially ambiguous weighted automata have the same expressive power. Moreover, we obtain such equivalence results for suitable weighted sublogics and finitely ambiguous or unambiguous aperiodic weighted automata. Our results hold for general weight structures, including all semirings, average computations of costs, bounded lattices, and others.

I&C Journal 2018 Journal Article

An automata-theoretic approach to the verification of distributed algorithms

• C. Aiswarya
• Benedikt Bollig
• Paul Gastin

We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e. g. , elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, which allow processes to exchange pids, store them in registers, and compare their register contents. To specify correctness properties, we introduce a logic that can reason about processes and pids. We show that model checking distributed algorithms can be reduced to satisfiability in propositional dynamic logic with loop and converse. Using this reduction, we provide an automata-theoretic approach to proving distributed algorithms correct up to a given number of rounds. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.

TCS Journal 2015 Journal Article

Checking conformance for time-constrained scenario-based specifications

• S. Akshay
• Paul Gastin
• Madhavan Mukund
• K. Narayan Kumar

We consider the problem of model checking message-passing systems with real-time requirements. As behavioral specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behavior can be regarded as a timed automaton. Our goal is to verify that all timed behaviors exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking/conformance problem.

Highlights Conference 2015 Conference Abstract

Tutorial: Weighted Automata: Highlighted Excerpts

• Paul Gastin

This talk will focus on a few highlights from the huge theory of weighted automata (WA). First, we introduce weighted automata and show how they can be used to model quantitative aspects of systems. This model is extremely versatile and by varying the weights/computations it can be used to describe counting, probabilities, optimizations, average power consumption, etc. We focus on sequential finite behaviors (words), and quickly discuss a few extensions (infinite words, trees, pebble-walking automata). We also investigate a few decision problems: emptiness, threshold, equivalence, recognizability of the support, etc. Second, we concentrate on weights/computations arising from a semiring. Actually, weighted automata were originally studied in this setting only, giving rise to an extensive theory of WA and formal power series (FPS), i. e. , quantitative functions over words. This special case allows for specific algorithms/definitions/results. For instance, a weighted automaton can be represented by a morphism to the monoid of matrices. The value/semantics of a WA can be computed efficiently using products of vectors/matrices (linear in the size of the input word, quadratic in the size of the automaton). Further, when the semiring is a field (possibly non-commutative), we will explain how to minimize a WA. As a consequence, the equivalence problem is decidable for WA over a subsemiring of a field. Last, the semiring structure allows one to define a (Cauchy) product of FPS and to obtain the equivalence between functions (FPS) that can be computed by WA and functions that can be denoted by weighted rational expressions. This extension of Kleene’s result is known as Schützenberger's theorem. Third, we will survey how weighted logics have been developed to match the quantitative expressive power of WA. The story started 10 years ago with the introduction of a quantitative (semiring) semantics for MSO logic over finite words and an equivalence theorem between weighted automata and a restricted weighted MSO logic. Since then, many extensions have been studied. Some extend the structure from words to trees, infinite words, pictures, etc. Others concern the quantitative aspect, moving from semirings to more general weights/computations. Also, the proof techniques have matured, from low level, carefully mimicking the classical proofs in the boolean setting, to higher level, using various abstract semantics. We illustrate this evolution by introducing a core weighted logic and its abstract semantics as multisets of weight structures. The equivalence between weighted automata and core weighted logic holds at the level of the abstract semantics. Most existing results can be derived easily.

TCS Journal 2014 Journal Article

Adding pebbles to weighted automata: Easy specification & efficient evaluation

• Paul Gastin
• Benjamin Monmege

We extend weighted automata and weighted rational expressions with 2-way moves and reusable pebbles. We show with examples from natural language modeling and quantitative model-checking that weighted expressions and automata with pebbles are more expressive and allow much more natural and intuitive specifications than classical ones. We extend Kleene–Schützenberger theorem showing that weighted expressions and automata with pebbles have the same expressive power. We focus on an efficient translation from expressions to automata. We also prove that the evaluation problem for weighted automata can be done very efficiently if the number of reusable pebbles is low.

MFCS Conference 2011 Conference Paper

Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking

• Benedikt Bollig
• Aiswarya Cyriac
• Paul Gastin
• Marc Zeitoun

Abstract We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and that, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.

I&C Journal 2010 Journal Article

Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces

• Paul Gastin
• Dietrich Kuske

We continue our study of the complexity of MSO-definable local temporal logics over concurrent systems that can be described by Mazurkiewicz traces. In previous papers, we showed that the satisfiability problem for any such logic is in PSPACE (provided the dependence alphabet is fixed, Gastin and Kuske (2003) [10]) and remains in PSPACE for all classical local temporal logics even if the dependence alphabet is part of the input, Gastin and Kuske (2007) [8]. In this paper, we consider the uniform satisfiability problem for arbitrary MSO-definable local temporal logics. For this problem, we prove multi-exponential lower and upper bounds that depend on the number of alternations of set quantifiers present in the chosen MSO-modalities.

TCS Journal 2007 Journal Article

Weighted automata and weighted logics

• Manfred Droste
• Paul Gastin

Weighted automata are used to describe quantitative properties in various areas such as probabilistic systems, image compression, speech-to-text processing. The behaviour of such an automaton is a mapping, called a formal power series, assigning to each word a weight in some semiring. We generalize Büchi’s and Elgot’s fundamental theorems to this quantitative setting. We introduce a weighted version of MSO logic and prove that, for commutative semirings, the behaviours of weighted automata are precisely the formal power series definable with particular sentences of our weighted logic. We also consider weighted first-order logic and show that aperiodic series coincide with the first-order definable ones, if the semiring is locally finite, commutative and has some aperiodicity property.

TCS Journal 2006 Journal Article

From local to global temporal logics over Mazurkiewicz traces

• Volker Diekert
• Paul Gastin

We review some results on global and local temporal logic on Mazurkiewicz traces. Our main contribution is to show how to derive the expressive completeness of global temporal logic with respect to first-order logic [V. Diekert, P. Gastin, LTL is expressively complete for Mazurkiewicz traces, J. Comput. System Sci. 64 (2002) 396–418] from the similar result on local temporal logic [V. Diekert, P. Gastin, Pure future local temporal logics are expressively complete for Mazurkiewicz traces, in: M. Farach-Colton (Ed.), Proc. LATIN’04, Lecture Notes in Computer Science, Vol. 2976, Springer, Berlin, 2004, pp. 232–241, Full version available as Research Report LSV-05-22, Laboratoire Spécification et Vérification, ENS Cachan, France].

I&C Journal 2006 Journal Article

Pure future local temporal logics are expressively complete for Mazurkiewicz traces

• Volker Diekert
• Paul Gastin

The paper settles a long standing problem for Mazurkiewicz traces: the pure future local temporal logic defined with the basic modalities exists-next and until is expressively complete. This means every first-order definable language of Mazurkiewicz traces can be defined in a pure future local temporal logic. The analogous result with a global interpretation has been known, but the treatment of a local interpretation turned out to be much more involved. Local logics are interesting because both the satisfiability problem and the model checking problem are solvable in Pspace for these logics whereas they are non-elementary for global logics. Both, the (previously known) global and the (new) local results generalize Kamp’s Theorem for words, because for sequences local and global viewpoints coincide.

I&C Journal 2004 Journal Article

Local temporal logic is expressively complete for cograph dependence alphabets

• Volker Diekert
• Paul Gastin

Recently, local logics for Mazurkiewicz traces are of increasing interest. This is mainly due to the fact that the satisfiability problem has the same complexity as in the word case. If we focus on a purely local interpretation of formulae at vertices (or events) of a trace, then the satisfiability problem of linear temporal logics over traces turns out to be PSPACE-complete if the dependence alphabet is not part of the input. But now the difficult problem is to obtain expressive completeness results with respect to first order logic. The main result of the paper shows such an expressive completeness result, if the underlying dependence alphabet is a cograph, i. e. , if all traces are series parallel posets. Moreover, we show that this is the best we can expect: If the dependence alphabet is not a cograph, then we cannot express all first order properties in our setting.

MFCS Conference 2003 Conference Paper

Local LTL with Past Constants Is Expressively Complete for Mazurkiewicz Traces

• Paul Gastin
• Madhavan Mukund
• K. Narayan Kumar

Abstract To obtain an expressively complete linear-time temporal logic (LTL) over Mazurkiewicz traces that is computationally tractable, we need to intepret formulas locally, at individual events in a trace, rather than globally, at configurations. Such local logics necessarily require past modalities, in contrast to the classical setting of LTL over sequences. Earlier attempts at defining expressively complete local logics have used very general past modalities as well as filters (side-conditions) that “look sideways” and talk of concurrent events. In this paper, we show that it is possible to use unfiltered future modalities in conjunction with past constants and still obtain a logic that is expressively complete over traces.

MFCS Conference 2003 Conference Paper

LTL with Past and Two-Way Very-Weak Alternating Automata

• Paul Gastin
• Denis Oddoux

Abstract In this paper, we propose a translation procedure of PLTL (LTL with past modalities) formulas to Büchi automata using two-way very-weak alternating automata (2VWAA) as an intermiediary step. Our main result is an efficient translation of 2VWAA to generalized Büchi automata (GBA).

TCS Journal 2002 Journal Article

A truly concurrent semantics for a process algebra using resource pomsets

• Paul Gastin
• Michael Mislove

In this paper we study a process algebra whose semantics is based on true concurrency. In our model, actions are defined in terms of the resources they need to execute, which allows a simple definition of a weak sequential composition operator. This operator allows actions which do not share any resources to execute concurrently, while dependent actions have to occur sequentially. This weak sequential composition operator may be used to automatically parallelize a sequential process. We add the customary (strict) sequential composition and a parallel composition operator allowing synchronization on specified actions. Our language also supports a hiding operator that allows the hiding of actions and even of individual resources used by actions. Strict sequential composition and hiding require that we generalize from the realm of Mazurkiewicz traces to that of pomsets, since these operations introduce “over-synchronized” traces—ones for which a pair of independent actions may occur sequentially. Our language also supports recursion and our semantics makes the unwinding of recursion visible by the use of special resources used to label unwindings. This is done on purpose in order to make divergence observable, but the usual semantics that does not observe unwindings can be obtained by using the hiding operator to abstract away from these special resources. We give both an SOS-style operational semantics for our language, as well as a denotational semantics based on resource pomsets. Generalizing results from our earlier work in this area, we derive a congruence theorem for our language which shows that the SOS-style operational rules induce the same equivalence relation on the language as the denotational semantic map does. A corollary is that our denotational model is both adequate and fully abstract relative to the behavior function defined from our operational semantics. This behavior consists naturally of the strings of actions the process can perform. This work continues our study into modelling concurrency in the absence of nondeterminism. In particular, our language is deterministic.

TCS Journal 2002 Journal Article

Resource traces: a domain for processes sharing exclusive resources

• Paul Gastin
• Dan Teodosiu

The domain of partially terminated finite and infinite words is commonly used to give denotational semantics for process algebras such as CSP. In this well-known framework the denotational semantics of concurrency is derived via power-domains from that of non-deterministic choice and interleaving to the effect that the denotational semantics of a concurrent process is equal to the set of all its possible finite and infinite sequential behaviours. In this paper, we define a more versatile domain of the so-called finite and infinite resource traces which allows to capture the concurrent behaviour of a process and encode the static concurrency of a system directly into the domains definition. The approach we present refines the previous work of Diekert and Gastin (Lecture Notes in Computer Science, vol. 944, Springer, Berlin, pp. 15–26) on α- and δ-traces. We start with an alphabet of atomic actions, a set of resources, and a resource map assigning to each action the non-empty subset of resources it uses. Actions that do not share common resources are called independent and considered to be able to execute concurrently. A partially terminated concurrent process is specified by a resource trace which consists of two components: an already observed part represented as an action-labeled partial order (Mazurkiewicz trace), and a guard set containing the resources granted to the process for its further development. A process concatenation is then defined, which allows independent actions to execute concurrently. Specification refinement leads to a natural approximation ordering between processes. It confers to the set of all processes the structure of a coherently complete prime algebraic Scott domain, whereby, process concatenation is Scott-continuous in both arguments. Furthermore, we define a natural ultrametric on processes based on prefix information. The induced topology is shown to be equivalent to the compact Lawson topology induced by the approximation ordering. Process concatenation is moreover shown to be uniformly continuous with respect to the defined ultrametric. The mathematical theory we develop thus extends the central order and metric properties of the domain of partially terminated finite and infinite words which are needed in order to devise truly concurrent semantics for process algebras much in the style of classical CSP semantics.

LPAR Conference 2001 Conference Paper

Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets

• Volker Diekert
• Paul Gastin

Abstract Recently, local logics for Mazurkiewicz traces are of increasing interest. This is mainly due to the fact that the satisfiability problem has the same complexity as in the word case. If we focus on a purely local interpretation of formulae at vertices (or events) of a trace, then the satisfiability problem of linear temporal logics over traces turns out to be PSPACE-complete. But now the dificult problem is to obtain expressive completeness results with respect to first order logic. The main result of the paper shows such an expressive completeness result, if the underlying dependence alphabet is a cograph, i. e. , if all traces are series parallel graphs. Moreover, we show that this is the best we can expect in our setting: If the dependence alphabet is not a cograph, then we cannot express all first order properties.

TCS Journal 2000 Journal Article

Asynchronous cellular automata for pomsets

• Manfred Droste
• Paul Gastin
• Dietrich Kuske

This paper extends to pomsets without auto-concurrency the fundamental notion of asynchronous cellular automata (ACA) which was originally introduced for traces by Zielonka. We generalize to pomsets the notion of asynchronous mapping introduced by Cori, Métivier and Zielonka and we show how to construct a deterministic ACA~from an asynchronous mapping. Then we investigate the relation between the expressiveness of monadic second-order logic, nondeterministic ACAs and deterministic ACAs. We can generalize Büchi's theorem for finite words to a class of pomsets without auto-concurrency which satisfy a natural axiom. This axiom ensures that an asynchronous cellular automaton works on the pomset as a concurrent read and exclusive owner write machine. More precisely, in this class nondeterministic ACAs, deterministic ACAs and monadic second-order logic have the same expressive power. Then we consider a class where deterministic ACAs are strictly weaker than nondeterministic ones. But in this class nondeterministic ACAs still capture monadic second-order logic. Finally, it is shown that even this equivalence does not hold in the class of all pomsets since there the class of recognizable pomset languages is not closed under complementation.

CSL Conference 1999 Conference Paper

A Truly Concurrent Semantics for a Simple Parallel Programming Language

• Paul Gastin
• Michael W. Mislove

Abstract This paper represents the beginning of a study aimed at devising semantic models for true concurrency that provide clear distinctions between concurrency, parallelismand choice. We present a simple programming language which includes (weakly) sequential composition, asynchronous and synchronous parallel composition, a restriction operator, and that supports recursion. We develop an operational and a denotational semantics for this language, and we obtain a theorem relating the behavior of a process as described by the transition system to the meaning of the process in the denotational model. This implies that the denotational model is adequate with respect to the operational model. Our denotational model is based on the resource traces of Gastin and Teodesiu, and since a single resource trace represents all possible executions of a concurrent process, we are able to model each term of our concurrent language by a single trace. Therefore we obtain a deterministic semantics for our language and we are able to model parallelism without introducing nondeterminism.

CSL Conference 1999 Conference Paper

An Expressively Complete Temporal Logic without Past Tense Operators for Mazurkiewicz Traces

• Volker Diekert
• Paul Gastin

Abstract Mazurkiewicz traces are a widely accepted model of concur- rent systems. We introduce a linear time temporal logic LTLf which has the same expressive power as the first order theory FO(<) of finite (in- finite resp.) traces. The main contribution of the paper is that we only use future tense modalities in order to obtain expressive completeness. Our proof is direct using no reduction to words and Kamp’s theorem for both finite and infinite words becomes a corollary. This direct approach became possible due to a proof technique of Wilke developed for the case of finite words.

I&C Journal 1999 Journal Article

The Kleene–Schützenberger Theorem for Formal Power Series in Partially Commuting Variables

• Manfred Droste
• Paul Gastin

Kleene's theorem on the coincidence of regular and rational languages in free monoids has been generalized by Schützenberger to a description of the recognizable formal power series in noncommuting variables over arbitrary semirings and by Ochmański to a characterization of the recognizable languages in trace monoids. We will describe the recognizable formal power series over arbitrary semirings and in partially commuting variables, i. e. over trace monoids. We prove that the recognizable series are certain rational power series, which can be constructed from the polynomials by using the operations sum, product, and a restricted star which is applied only to series for which the elements in the support all have the same connected alphabet. The converse is true if the underlying semiring is commutative. Moreover, if in addition the semiring is idempotent then the same result holds with a star restricted to series for which the elements in the support have connected (possibly different) alphabets. It is shown that these assumptions over the semiring are necessary. This provides a joint generalization of Kleene's, Schützenberger's and Ochmański's theorems.

MFCS Conference 1998 Conference Paper

A (Non-elementary) Modular Decision Procedure for LTrL

• Paul Gastin
• Raphaël Meyer
• Antoine Petit 0001

Abstract Thiagarajan and Walukiewicz [18] have defined a temporal logic LTrL on Mazurkiewicz traces, patterned on the famous propositional temporal logic of linear time LTL defined by Pnueli. They have shown that this logic is equal in expressive power to the first order theory of finite and infinite traces. The hopes to get an ”easy” decision procedure for LTrL, as it is the case for LTL, vanished very recently due to a result of Walukiewicz [19] who showed that the decision procedure for LTrL is non-elementary. However, tools like Mona [8] or Mosel [7] show that it is possible to handle non-elementary logics on significant examples. Therefore, it appears worthwhile to have a direct decision procedure for LTrL; in this paper we propose such a decision procedure, in a modular way. Since the logic LTrL is not pure future, our algorithm constructs by induction a finite family of Büchi automata for each LTrL-formula. As expected by the results of [19], the main difficulty comes from the ”Until” operator.

MFCS Conference 1995 Conference Paper

On Congruences and Partial Orders

• Serge Bauget
• Paul Gastin

Abstract Mazurkiewicz trace theory is not powerful enough to describe concurrency paradigms as, for instance, the “Producer / Consumer”. We propose in this paper a generalization of Mazurkiewicz trace monoids which allows to model such problems. We consider quotients of the free monoids by congruences which preserve the commutative images of words. An equivalence class in the quotient monoid consists of all the sequential observations of a distributed computation. In order to characterize congruences which do model concurrency, we study the relationship of this approach and the classical representation of distributed computations with partial orders. We show that the only congruences for which the classes can be represented by partial orders and the concatenation transfers modularly to partial orders are congruences generated by commutations, that is trace congruences. We prove necessary conditions and sufficient conditions on congruences so that their classes can be represented by partial orders. In particular, an important sufficient condition covers both trace congruences and the “Producer / Consumer” congruence.

TCS Journal 1995 Journal Article

Preface

• Paul Gastin
• Jan Rutten

TCS Journal 1994 Journal Article

An extension of Kleene's and Ochmański's theorems to infinite traces

• Paul Gastin
• Antoine Petit
• Wiesław Zielonka

As was noted by Mazurkiewicz, traces constitute a convenient tool for describing finite behaviour of concurrent systems. Extending in a natural way Mazurkiewicz's original definition, infinite traces have recently been introduced enabling one to deal with infinite behaviour of nonterminating concurrent systems. In this paper we examine the basic families of recognizable sets and of rational sets of infinite traces. The seminal Kleene characterization of recognizable subsets of the free monoid and its subsequent extensions to infinite words due to Büchi and to finite traces due to Ochmański are the cornerstones of the corresponding theories. The main result of our paper is an extension of these characterizations to the domain of infinite traces. Using recognizing and weakly recognizing morphisms, as well as a generalization of the Schützenberger product of monoids, we prove various closure properties of recognizable trace languages. Moreover, we establish normal-form representations for recognizable and rational sets of infinite traces.

TCS Journal 1993 Journal Article

The poset of infinitary traces

• Paul Gastin
• Brigitte Rozoy

Partially commutative monoids, also called trace monoids, are among the most-studied formalisms to describe the behaviour of distributed systems. In order to model systems which never stop, we have to consider an extension of traces, namely infinite traces. Finite-trace monoids are strongly related to partial-order sets (PoSets), domains and event structures, which are other models to describe the behaviour of distributed systems. The aim of this paper is to establish similar connexions between infinite-trace monoids, PoSets and event structures. We prove that the set of finite and infinite traces with the prefix order is a Scott domain and a coherently complete prime algebraic PoSet. Moreover, we establish a representation theorem between the class of finite- and infinite-trace PoSets and a subclass of labelled prime event structures.

MFCS Conference 1992 Conference Paper

Poset Properties of Complex Traces

• Paul Gastin
• Antoine Petit 0001

Abstract This paper investigates PoSct properties of the monoid ℂ of infinite dependence graphs and of the monoid ℂ of complex traces. We show that a subset of G admits a least upper bound if and only if this set is coherent and countable. Hence, G is bounded complete. The compact and the prime graphs in G arc characterized and we prove that each graph is the least upper bound of its compact (resp. its prime) lower bounds. Therefore, up to the restriction to countable sets, G is a coherently complete Scott-Domain and is Prime Algebraic. We define very naturally two orders on ℂ: the product order and the prefix order. We show that ℂ with each order is a coherently complete CPO and we characterize the least upper bound (the greatest lower bound resp.) of a subset of ℂ when it exists. But contrary to the case of G, we prove that ℂ is not a Scott-Domain in general.

MFCS Conference 1991 Conference Paper

Recognizable Complex Trace Languages

• Volker Diekert
• Paul Gastin
• Antoine Petit 0001

Abstract A. Mazurkiewicz defined traces in order to modelize non-sequential processes. Complex traces have been recently introduced as a generalization of both traces and infinite words. This paper studies the family of recognizable complex trace languages. It is proved that this family is closed under boolean operations, concatenation, left and right quotients. Then sufficient conditions ensuring the recognizability of the finite and infinite iterations of a recognizable complex trace language are given. The notion of co-iteration is defined and the Kleene-Ochmanski theorem is generalized to complex traces.

TCS Journal 1990 Journal Article

Un modèle asynchrone pour les systèmes distribués

• Paul Gastin

Many researchers are engaged in the field of distributed systems modelization. We present a new model inspired by the language theory. Its particularity within this theory is the rejection of interleaving for the representation of concurrency. Here, the main ideas are born from languages such as CSP or ESTELLE. The point is mainly the real lack of dependency between processes apart from synchronisations, which are rendez-vous. Once the model is defined, we introduce, as in the infinitary free monoïd, notions such as length, concatenation, prefix order, upper bound and infinite product. So the distributed model is provided with all the operations necessary to develop semantics. Then, we prove that the finitary part of the distributed model is isomorphic to the free partially commutative monoïd (fpcm). Finally, we settle the bases of an infinitary extension of the fpcm.