Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces

Adsul, Bharat; Gastin, Paul; Kulkarni, Shantanu

doi:10.4230/LIPIcs.CONCUR.2025.5

Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces

Bharat Adsul

IIT Bombay, Mumbai, India Paul Gastin

Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-sur-Yvette, France
CNRS, ReLaX, IRL 2000, Siruseri, India Shantanu Kulkarni

IIT Bombay, Mumbai, India

Abstract

We study fragments of temporal logics over Mazurkiewicz traces which are well known and established partial-order models of concurrent behaviours. We focus on concurrent versions of “strict past” and “strict future” modalities. Over words, the corresponding fragments have been shown to coincide with natural algebraic conditions on the recognizing monoids. We provide non-trivial generalizations of these classical results to traces. We exploit the local nature of the temporal modalities and obtain modular translations of specifications into asynchronous automata. More specifically, we provide novel characterizations of these fragments via local cascade products of a very simple two-state asynchronous automaton operating on a single process.

Keywords and phrases:

Mazurkiewicz traces, temporal logics, asynchronous automata, cascade product, Green’s relations, algebraic automata theory

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Modal and temporal logics ; Theory of computation

\rightarrow

Distributed computing models ; Theory of computation

\rightarrow

Algebraic language theory ; Security and privacy

\rightarrow

Logic and verification

DOI:

10.4230/LIPIcs.CONCUR.2025.5

Event:

36th International Conference on Concurrency Theory (CONCUR 2025)

Editors:

Patricia Bouyer and Jaco van de Pol

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Temporal logics are widely used logical formalisms to reason about properties of computations. Words serve as temporal models of sequential computations/behaviours and linear temporal logic LTL formulas use natural future as well as past temporal modalities to talk about interesting patterns of these behaviours. The celebrated theorem of Kamp [16] showed that, over words, properties definable in LTL coincide with those definable in the first order (FO) logic. By the seminal results of McNaughton-Papert [18] and Schutzenberger [20], these also equal regular languages describable by star-free regular expressions and those recognized by finite aperiodic monoids.

The above mentioned results clearly indicate the important role played by the temporal modalities in the very rich expressive power of LTL. Natural and commonly used temporal modalities include future modalities $\mathop{\mathsf{X}\vphantom{a}}\nolimits$ (“neXt/tomorrow”), $\mathop{\mathsf{F}\vphantom{a}}\nolimits$ (“Future”), $\mathop{\mathsf{U}\vphantom{a}}\nolimits$ (“Until”), the past counterparts $\mathop{\mathsf{Y}\vphantom{a}}\nolimits$ (“previous/Yesterday”), $\mathop{\mathsf{P}\vphantom{a}}\nolimits$ (“Past”), $\mathop{\mathsf{S}\vphantom{a}}\nolimits$ (“Since”) and their strict variants such as $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ (“strict future”) and $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ (“strict past”). Several works $\cite[cite]{[\@@bibref{}{COHEN1993271}{}{}]},\cite[cite]{[\@@bibref{}{ETESSAMI% 200088}{}{}]},\cite[cite]{[\@@bibref{}{bojanczyk2020% languagesrecognisedfinitesemigroups}{}{}]}$ have studied natural fragments of LTL obtained by allowing only some of these modalities and have characterized these fragments in terms of algebraic conditions on the recognizing finite monoids. These algebraic characterizations have been crucially used to show that the computational problems of definability in the associated fragments are decidable.

Let us consider the fragment $\mathsf{LTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ obtained by allowing only unary strict past modality $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ . When interpreted over words, the formula $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ $\varphi$ , at a given position, asserts that $\varphi$ holds at some position in the strict past (that is, strictly left) of the current position. It has been shown in $\cite[cite]{[\@@bibref{}{BRZOZOWSKIRTRIVIAL}{}{}]},\cite[cite]{[\@@bibref{}{% COHEN1993271}{}{}]},\cite[cite]{[\@@bibref{}{ETESSAMI200088}{}{}]},\cite[cite]% {[\@@bibref{}{bojanczyk2020languagesrecognisedfinitesemigroups}{}{}]}$ that a language is definable in $\mathsf{LTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ iff it can be recognized by a $\mathcal{R}$ -trivial monoid iff the syntactic monoid of the language is $\mathcal{R}$ -trivial. Here $\mathcal{R}$ stands for one of fundamental Green’s relations on a monoid. The $\mathcal{R}$ -triviality condition on a monoid $M$ simply means that if two elements of $M$ are right multiples of each other then they are equal (that is, for all $m,n\in M$ , $\exists\;p,q\in M:n=m\cdot p\mbox{\leavevmode\nobreak\ and\leavevmode\nobreak% \ }m=n\cdot q$ implies $m=n$ ). This characterization can also be stated in simpler automata-theoretic terms [6]. A finite-state automaton is said to be partially ordered if there is a partial order $\succeq$ on the states so that every transition is of the form $(p,a,q)$ where $p\succeq q$ . Said differently, an automaton is partially ordered iff the only cycles present in the underlying directed transition graph are self loops. Using this notion, the above mentioned characterization can be stated as follows: a language is $\mathsf{LTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ -definable iff it can be accepted by a partially ordered automaton.

It turns out that the dual fragment $\mathsf{LTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ which admits the unary strict future modality $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ is characterized by the dual condition of $\mathcal{L}$ -triviality. As expected, a monoid is $\mathcal{L}$ -trivial if no two distinct elements can be left multiples of each other. The fragment $\mathsf{LTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ which includes both $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ and $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ modalities has been well studied and is known to coincide with important first order logic fragments, namely, $FO^{2}$ and $\Delta_{2}$ . It also has an algebraic characterization in terms of monoids from the class DA. See the survey [9] for more details.

In this work we study the above mentioned temporal logic fragments from the concurrency viewpoint. We consider Mazurkiewicz traces as the underlying models of concurrent behaviours. A Mazurkiewicz trace or simply trace, over a set of processes, represents a concurrent behaviour as a labelled partial-order between events. This partial-order between events faithfully captures the causal information flow among processes. Traces are extensively studied and there is a rich theory of regular trace languages $\cite[cite]{[\@@bibref{}{Zielonka-RAIRO-TAI-87}{}{}]},\cite[cite]{[\@@bibref{}% {TraceBook-DR-1995}{}{}]}$ . Regular trace languages are known to coincide with MSO-definable languages as well as languages recognized by finite monoids. We consider natural event-based interpretations of temporal modalities $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ and $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ over traces. For instance, the formula $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ $\varphi$ , at a given event, asserts that $\varphi$ holds at an event which is in the strict causal past of the current event. We denote by $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ the local/event-based temporal logic over traces which has access to the temporal modality $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ . One can similarly define $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ and $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ . One of our main results states that a trace language is definable in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ iff it can be recognized by a $\mathcal{R}$ -trivial monoid. This can be viewed as a non-trivial generalization of the corresponding result over words. We also obtain an analogous algebraic characterization of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ in terms of $\mathcal{L}$ -trivial monoids. An algebraic characterization of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ in terms of monoids from the class DA already appears in [17].

Another important contribution of this work is a modular translation of formulas in these fragments into asynchronous automata. In an asynchronous automaton, each process runs a finite local-state device and these devices synchronize with each other on shared actions. Asynchronous automata can be naturally used to accept trace languages. Zielonka’s theorem states that regular trace languages are precisely the languages accepted by asynchronous automata. As in [19, 2, 3], one can use asynchronous automata as transducers on traces, similar in spirit to the sequential letter-to-letter transducers on words. Unlike these works which use deterministic asynchronous transducers to locally compute relabelling functions on input traces, we allow non-deterministic asynchronous transducers. As expected, these transducers compute relabelling relations from input traces to output traces. The local cascade product of deterministic asynchronous automata (or transducers) from [2, 3] is a natural generalization of cascade product in the sequential setting [21]. It further extends naturally to the non-deterministic setting and corresponds to compositions of related relabelling relations.

We use this machinery to provide a translation (in fact, a characterization) of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ formulas into local cascade products of very simple two-state asynchronous automata operating on a single process. For $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ formulas, the resulting atomic two-state transducers are deterministic while for $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ formulas, they are reverse-deterministic. We remark that our results and their proofs for traces specialize to the setting of words.

The rest of the paper is organized as follows. After setting up the preliminary notions in Section 2, we establish in Section 3 that $\mathcal{R}$ -trivial trace languages are definable in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ . In Section 4, we provide a translation of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ formulas into cascade products of localized deterministic asynchronous transducers/automata whose transition monoid is isomorphic to $U_{1}$ - the unique two element aperiodic monoid. Section 5 is devoted to dual results concerning $\mathcal{L}$ -trivial and $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ -definable trace languages. We also sketch a cascade product based characterization of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ in this section.

2 Preliminaries

In this section, we set up the notation and review basics of traces. We also recall the recognizability of trace languages by morphisms into monoids and define the fundamental Green’s relations on monoids.

2.1 Trace basics

Let $\mathscr{P}$ be a finite, non-empty set of processes. For every process $i\in\mathscr{P}$ , $\Sigma_{i}$ is the set of letters/actions in which process $i$ participates. A distributed alphabet over $\mathscr{P}$ is the family $\tilde{\Sigma}=\{\Sigma_{i}\}_{i\in\mathscr{P}}$ with $\Sigma=\cup_{i\in\mathscr{P}}\Sigma_{i}$ being the associated total alphabet. Letters $a,b\in\Sigma$ are dependent if there is a process which participates in both of them ( $\exists i\in\mathscr{P}$ , $a,b\in\Sigma_{i}$ ), otherwise they are independent. For a letter $a\in\Sigma$ we define $\mathsf{loc}(a)=\{i\in\mathscr{P}\mid a\in\Sigma_{i}\}$ to be the set of processes that participate in $a$ .

A poset is a tuple $(E,\leq)$ with $E$ being the underlying set and $\leq$ being the partial order on $E$ . A $\Sigma$ -labelled poset over $\tilde{\Sigma}$ is a triple $(E,\leq,\lambda)$ where $(E,\leq)$ is the underlying poset, and $\lambda\colon E\to\Sigma$ is the labelling function which labels each element in $E$ with a letter from $\Sigma$ . For elements $e,e^{\prime}\in E$ , $e^{\prime}$ is said to be an immediate successor of $e$ , denoted by $e\lessdot e^{\prime}$ , if $e$ is below $e^{\prime}$ ( $e<e^{\prime}$ ) and there is no event $f$ strictly between $e$ and $e^{\prime}$ ( $\nexists f\in E$ , $e<f<e^{\prime}$ ).

A (Mazurkiewicz) trace $t=(E,\leq,\lambda)$ over $\tilde{\Sigma}$ is a finite $\Sigma$ -labelled poset with $\lambda$ satisfying the following two properties:

1.

for $e,e^{\prime}\in E$ , if $e\lessdot e^{\prime}$ , then $\lambda(e)$ and $\lambda(e^{\prime})$ are dependent;
2.

for $e,e^{\prime}\in E$ , if $\lambda(e)$ and $\lambda(e^{\prime})$ are dependent, then they are ordered ( $e\leq e^{\prime}$ or $e^{\prime}\leq e$ ).

For a trace $t=(E,\leq,\lambda)$ we sometimes slightly abuse notation to say event $e\in t$ which we take to mean that event $e\in E$ . The set of process $i$ -events in $t$ is defined as $E_{i}=\{e\in E\mid\lambda(e)\in\Sigma_{i}\}$ . Note that $E_{i}$ is totally ordered by $\leq$ . For an event $e\in t$ , we slightly abuse the notation and define $\mathsf{loc}(e)=\mathsf{loc}(\lambda(e))$ to be the set of processes that participate in $e$ . For an event $e$ we define ${\downarrow}e=\{f\in t\mid f\leq e\}$ to be the set of events in $t$ below $e$ . Similarly ${\Downarrow}e=\{f\in t\mid f<e\}$ is the set of events in $t$ strictly below $e$ . It is easy to see that by restricting $\leq$ and $\lambda$ to events in ${\downarrow}e$ , we obtain a valid trace. By abuse of notation, we denote this trace by $({\downarrow}e,\leq,\lambda)$ or simply ${\downarrow}e$ . It will be clear from the context whether we mean ${\downarrow}e$ to be a trace or merely a set of events. Similarly, ${\Downarrow}e$ also refers to the trace $({\Downarrow}e,\leq,\lambda)$ induced by ${\Downarrow}e$ .

The set of all finite traces over $\tilde{\Sigma}$ is denoted by $TR(\tilde{\Sigma})$ . We define the trace concatenation operation $\cdot$ on $TR(\tilde{\Sigma})$ as follows. Let $t_{1}=(E_{1},\leq_{1},\lambda_{1}),t_{2}=(E_{2},\leq_{2},\lambda_{2})\in TR(% \tilde{\Sigma})$ with $E_{1}\cap E_{2}=\emptyset$ . We define $t_{1}\cdot t_{2}$ or simply $t_{1}t_{2}$ to be the trace $(E_{1}\cup{E_{2}},\leq,\lambda)\in TR(\tilde{\Sigma})$ where:

1.

$\leq$ is the transitive closure of ${\leq}_{1}\cup{\leq}_{2}\cup\{(e_{1},e_{2})\in E_{1}\times E_{2}\mid\lambda_{1% }(e_{1}),\lambda_{2}(e_{2})\text{ are dependant}\}$ .
2.

For all $e\in E_{1}\cup E_{2}$ , $\lambda(e)=\lambda_{1}(e)\text{ if }e\in E_{1}\text{ and }\lambda_{2}(e)\text{% if }e\in E_{2}.$

A trace $t^{\prime}$ is said to be a prefix of trace $t$ if there exists $t^{\prime\prime}\in TR(\tilde{\Sigma})$ such that $t=t^{\prime}t^{\prime\prime}$ . It is easy to see that, for $e\in t$ , ${\downarrow}e$ and ${\Downarrow}e$ are both prefixes of $t$ .

2.2 Recognizable trace languages

Recall that a monoid is a set $M$ equipped with a binary associative operation $\cdot$ and containing an identity element $1_{M}$ , such that $\forall m\in M$ , $m\cdot 1_{M}=1_{M}\cdot m=m$ . The set $TR(\tilde{\Sigma})$ , under the operation of trace concatenation, is a monoid with the empty trace $\varepsilon$ as the identity element. Let $M$ and $N$ be two monoids with operations $\cdot$ and $\circ$ respectively. A morphism $h$ from $M$ to $N$ is a map $h\colon M\to N$ such that: $h(1_{M})=1_{N}$ and for all $m_{1},m_{2}\in M$ , $h(m_{1}\cdot m_{2})=h(m_{1})\circ h(m_{2})$ .

A subset $L\subseteq TR(\tilde{\Sigma})$ is called a trace language over $\tilde{\Sigma}$ . We call a morphism from the trace monoid $TR(\tilde{\Sigma})$ to any other monoid $M$ as a trace morphism. A trace language $L\subseteq TR(\tilde{\Sigma})$ is recognizable if there exists a trace morphism $h$ from $TR(\tilde{\Sigma})$ to a finite monoid $M$ such that $L=\cup_{m\in P}h^{-1}(m)$ for some $P\subseteq M$ . We may refer to $h$ as the recognizing morphism or say that $L$ is recognized by $M$ via recognizing morphism $h$ . The class of recognizable trace languages, also referred to as regular trace languages, has several characterizations and we note a few in particular, namely MSO-definable languages over traces [22] and trace languages accepted by asynchronous automata [23].

Classically, the algebraic viewpoint in terms of what are known as Green’s relations over monoids has been fruitful for characterizing interesting subclasses of regular languages which have an intimate connection with logics. We now briefly recall these fundamental Green’s preorders and the associated equivalence relations.

Let $M$ be a monoid with $\cdot$ as the binary monoid operation and let $m_{1},m_{2}\in M$ . The Green’s preorder relations are defined as follows:

1.

$m_{1}\leq_{R}m_{2}$ (read as $m_{1}$ is $R$ -below $m_{2}$ ) if there exists $m\in M$ such that $m_{1}=m_{2}\cdot m$ .
2.

$m_{1}\leq_{L}m_{2}$ if there exists $m\in M$ such that $m_{1}=m\cdot m_{2}$ .
3.

$m_{1}\leq_{J}m_{2}$ if there exist $u,v\in M$ such that $m_{1}=u\cdot m_{2}\cdot v$
4.

$m_{1}\leq_{H}m_{2}$ if $m_{1}\leq_{R}m_{2}$ and $m_{1}\leq_{L}m_{2}$

These preorders naturally give rise to the associated equivalence relations $\mathcal{R},\mathcal{L},\mathcal{J},\mathcal{H}$ . We say that $m_{1}\mathrel{\mathcal{R}}m_{2}$ (read as $m_{1}$ is $\mathcal{R}$ -equivalent to $m_{2}$ ) if $m_{1}\leq_{R}m_{2}$ and $m_{2}\leq_{R}m_{1}$ . A monoid $M$ is $\mathcal{R}$ -trivial if $\forall m_{1},m_{2}\in M$ , $m_{1}\mathrel{\mathcal{R}}m_{2}$ implies $m_{1}=m_{2}$ . In other words, $M$ is $\mathcal{R}$ -trivial iff the preorder $\leq_{R}$ on $M$ is in fact a partial order on $M$ iff the equivalence relation $\mathcal{R}$ coincides with the identity relation on $M$ .

The other equivalence relations $\mathcal{L},\mathcal{J},\mathcal{H}$ and their triviality for $M$ are defined analogously. A trace language $L\subseteq TR(\tilde{\Sigma})$ is called $\mathcal{R}$ -trivial if it can be recognized by a finite $\mathcal{R}$ -trivial monoid. One can similarly define $\mathcal{L}$ -trivial, $\mathcal{J}$ -trivial and $\mathcal{H}$ -trivial trace languages.

Example 1.

Consider the monoid $U_{1}=\{1,0\}$ with $1$ as the identity and $0$ as the zero element. So, $1\cdot 1=1$ , $0\cdot 1=1\cdot 0=0\cdot 0=0$ . It is easily checked that $U_{1}$ is $\mathcal{R}$ -trivial, $\mathcal{L}$ -trivial, $\mathcal{J}$ -trivial as well as $\mathcal{H}$ -trivial.

As mentioned in the introduction, for word languages, $\mathcal{R}$ -triviality ( $\mathcal{L}$ -triviality) corresponds to definability in LTL with only the strict past (respectively strict future) modality. See [5] for a proof based on Green’s relations. It turns out that, for finite monoids, $\mathcal{H}$ -triviality condition is equivalent to the aperiodicity property. As a consequence, $\mathcal{H}$ -trivial word languages coincide with languages definable in the first order logic and linear temporal logic. These results find interesting generalizations over traces in [15, 13, 8].

3 Algebra to temporal logic

We now state our main theorem and set up the technical machinery and prove it.

Theorem 2.

Let $L\subseteq TR(\tilde{\Sigma})$ . Then the following are equivalent.

1.

$L$ is a $\mathcal{R}$ -trivial trace language.
2.

$L$ can be expressed using a sentence in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ .
3.

$L$ can be accepted by a cascade product of localized $U_{1}$ asynchronous automata.

Proof.

$1\to 2$ is shown in Theorem 14, $2\to 3$ is shown in Theorem 22, $3\to 1$ is shown in Theorem 24. $\hfill\blacktriangleleft$

The result we wish to prove in this section is the $1\to 2$ for Theorem 2, which says that any trace language which is recognized by a $\mathcal{R}$ -trivial monoid can be expressed as a sentence in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ . This statement is restated as Theorem 14. We start by defining formally the syntax and semantics of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ .

3.1 $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ syntax and semantics

We now define $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ . We have sentences $\Phi$ , which are evaluated over finite Mazurkiewicz traces and hence define languages over $TR(\tilde{\Sigma})$ and also event formulas $\varphi$ which are evaluated at a given event in a trace. The syntax is as follows:

	$\displaystyle\Phi$	$\displaystyle::=\mathop{\mathsf{E}\vphantom{a}}\nolimits\varphi\mid\Phi_{1}% \lor\Phi_{2}\mid\lnot\Phi$
	$\displaystyle\varphi$	$\displaystyle::=a\mid\varphi_{1}\lor\varphi_{2}\mid\lnot\varphi\mid\mathop{% \mathsf{YP}\vphantom{a}}\nolimits\varphi$

The semantics for the boolean operations are as usual. For a trace $t=(E,\leq,\lambda)$ and an event $e\in E$ , the following defines the semantics of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$

$\displaystyle t$	$\displaystyle\models\mathop{\mathsf{E}\vphantom{a}}\nolimits\varphi$	if there exists an event $e$ in $t$ such that $t,e\models\varphi$
$\displaystyle t,e$	$\displaystyle\models a$	if $\lambda(e)=a$
$\displaystyle t,e$	$\displaystyle\models\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi$	if there exists an event $f$ in $t$ with $f<e$ and $t,f\models\varphi$ .

In the rest of the paper we shall use the following macros liberally:

	$\displaystyle\mathop{\mathsf{A}\vphantom{a}}\nolimits\varphi$	$\displaystyle=\lnot\mathop{\mathsf{E}\vphantom{a}}\nolimits\lnot\varphi,$	$\displaystyle\mathop{\mathsf{P}\vphantom{a}}\nolimits\varphi$	$\displaystyle=\varphi\lor\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi,$
	$\displaystyle\mathop{\mathsf{YH}\vphantom{a}}\nolimits\varphi$	$\displaystyle=\lnot\mathop{\mathsf{YP}\vphantom{a}}\nolimits\lnot\varphi,$	$\displaystyle\mathop{\mathsf{H}\vphantom{a}}\nolimits\varphi$	$\displaystyle=\varphi\land\mathop{\mathsf{YH}\vphantom{a}}\nolimits\varphi\,.$

The modalities can be read as Exists $(\mathop{\mathsf{E}\vphantom{a}}\nolimits)$ , All $(\mathop{\mathsf{A}\vphantom{a}}\nolimits)$ , Past $(\mathop{\mathsf{P}\vphantom{a}}\nolimits)$ , Historically $(\mathop{\mathsf{H}\vphantom{a}}\nolimits)$ , Yesterday Past $(\mathop{\mathsf{YP}\vphantom{a}}\nolimits)$ , Yesterday Historically $(\mathop{\mathsf{YH}\vphantom{a}}\nolimits)$ . For a set of letters $A$ , we may abuse notation and use $A$ to denote the event formula $\bigvee_{a\in A}a$ testing whether the event is labelled by a letter in $A$ . For instance, we may use $\Sigma_{i}$ as the macro for the event formula $\bigvee_{a\in\Sigma_{i}}a$ which tests whether the current event is an $i$ -event.

Example 3.

Let $t\in TR(\tilde{\Sigma})$ be a trace and $e\in t$ be an event. We design an event formula $\varphi^{i}_{k}$ such that $t,e\models\varphi^{i}_{k}$ iff there are at least $k$ process $i$ -events strictly below event $e$ . We define $\varphi^{i}_{k}$ inductively as: $\varphi^{i}_{0}=\top$ and for $k>0$ , $\varphi^{i}_{k}=\mathop{\mathsf{YP}\vphantom{a}}\nolimits(\Sigma_{i}\land% \varphi^{i}_{k-1})$ . Consider the $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ sentence $\Phi_{m,n}=\mathop{\mathsf{E}\vphantom{a}}\nolimits(\Sigma_{j}\land\varphi^{j}% _{n-1}\land\lnot\varphi^{j}_{n}\land\varphi^{i}_{m})$ . Clearly $\Phi_{m,n}$ has the property that trace $t$ satisfies $\Phi_{m,n}$ if and only if the $m^{th}$ process $i$ -event is strictly below the $n^{th}$ process $j$ -event.

3.2 Critical structures for a morphism into a $\mathcal{R}$ -trivial monoid

Throughout the rest of this section, we fix a morphism $h\colon TR(\tilde{\Sigma})\rightarrow M$ to a fixed finite $\mathcal{R}$ -trivial monoid $M$ .

Let $t=(E,\leq,\lambda)$ be a trace and $e\in E$ be an event of $t$ . Note that, viewing ${\downarrow}e$ and ${\Downarrow}e$ as traces, we have $h({\downarrow}e)=h({\Downarrow}e)h(\lambda(e))\leq_{R}h({\Downarrow}e)$ . The event $e$ is said to be a critical event in $t$ if $h({\downarrow}e)\neq h({\Downarrow}e)$ . Since the monoid $M$ is $\mathcal{R}$ -trivial, this is equivalent to $h({\downarrow}e)<_{R}h({\Downarrow}e)$ . We let $X_{t}=\{e\in E\mid h({\downarrow}e)<_{R}h({\Downarrow}e)\}$ be the set of all critical events of trace $t$ .

Lemma 4.

In the above notation, $|X_{t}|<|\mathscr{P}|\times|M|$ .

Proof.

We show that the number of critical events on a single process line is less than $|M|$ . This clearly implies that $|X_{t}|$ is less than $|\mathscr{P}|\times|M|$ . For any $i\in\mathscr{P}$ , the set of critical process $i$ events is $X_{t}\cap E_{i}$ . Assume $X_{t}\cap E_{i}=\{e_{1},e_{2},\cdots e_{k}\}$ with $e_{1}<e_{2}<\cdots<e_{k}$ ( $E_{i}$ is totally ordered by $\leq$ ). Since $e_{j}$ are critical events we have $h({\downarrow}e_{j})<_{R}h({\Downarrow}e_{j})$ . Since (the trace induced by) ${\downarrow}e_{j}$ is a prefix of (the trace induced by) ${\Downarrow}e_{j+1}$ , we have $h({\Downarrow}e_{j+1})\leq_{R}h({\downarrow}e_{j})$ . We get

h({\downarrow}e_{k})<_{R}h({\Downarrow}e_{k})\leq_{R}h({\downarrow}e_{k-1})<_{% R}h({\Downarrow}e_{k-1})\leq_{R}\cdots h({\downarrow}e_{1})<_{R}h({\Downarrow}% e_{1})\leq_{R}1_{M}\,.

Therefore $k<|M|$ which concludes the proof. $\hfill\blacktriangleleft$

A configuration of $t$ is a subset $C\subseteq E$ of events which is downward closed: $C={\downarrow}C$ . Clearly, for any event $e\in E$ , ${\downarrow}e$ and ${\Downarrow}e$ are configurations of $t$ . We sometimes abuse the notation and use $C$ to also denote the trace induced by a configuration $C$ of $t$ . It is easy to see that $t=C\cdot t^{\prime}$ where $t^{\prime}$ is the trace induced by the set $E\setminus C$ of events of $t$ which do not belong to $C$ .

A configuration $C$ of $t$ is critical if for every maximal event $e\in C$ , we have $h(C)\neq h(C\setminus\{e\})$ , equivalently, $h(C)<_{R}h(C\setminus\{e\})$ . Note that if $e$ is a maximal event of $C$ then $C\setminus\{e\}$ is a configuration of $t$ .

Lemma 5.

Every maximal event of a critical configuration is a critical event.

Proof.

Suppose for contradiction that there exists a critical configuration $C$ and a maximal event $e\in C$ such that $h(C)<_{R}h(C\setminus\{e\})$ but $h({\downarrow}e)=h({\Downarrow}e)$ . We have that $h(C)=h({\downarrow}e)\cdot h(C\setminus{\downarrow}e)$ . Substituting $h({\downarrow}e)$ by $h({\Downarrow}e)$ , we get $h(C)=h({\Downarrow}e)\cdot h(C\setminus{\downarrow}e)=h(C\setminus\{e\})$ giving us a contradiction to the fact that $h(C)\neq h(C\setminus\{e\})$ . $\hfill\blacktriangleleft$

Example 6.

A configuration in which every maximal event is critical, may not itself be critical. We show this via an example. Consider three processes and the distributed alphabet defined by $\Sigma_{1}=\{a\}$ , $\Sigma_{2}=\{b\}$ and $\Sigma_{3}=\{c\}$ (each process has a local action). Consider the $\mathcal{R}$ -trivial (commutative) monoid $M=(\{0,1,2\},\oplus,0)$ with truncated sum defined as $x\oplus y=\min(2,x+y)$ . In other words, $0$ is the neutral element, $2$ is absorbent, and $1\oplus 1=2$ . We have $2<_{R}1<_{R}0$ . Consider the (truncated) length trace morphism $h\colon TR(\tilde{\Sigma})\to M$ defined by $h(x)=1$ for all $x\in\Sigma$ . Finally, let $t=abc=(E,\leq,\lambda)$ be the trace with 3 events labelled $a$ , $b$ and $c$ respectively. Each event $e$ in $t$ is critical and is maximal in $t$ . But the configuration $E$ is not critical since for each $e\in E$ , we have $h(E\setminus\{e\})=2=h(E)$ .

Lemma 7.

Any prefix $t^{\prime}$ of $t$ containing all the critical events of $t$ , evaluates to the same monoid value as $t$ under $h$ . In other words, we have $h({\downarrow}X_{t})=h(t)$ .

Proof.

We have $h(t)\leq_{R}h({\downarrow}X_{t})$ since ${\downarrow}X_{t}$ is a prefix of $t$ . For the converse, we first show that there exists a critical configuration $C$ of $t=(E,\leq,\lambda)$ such that $h(C)=h(t)$ . The configuration $C=E$ satisfies $h(C)=h(t)$ . Let $C$ be a configuration with $h(C)=h(t)$ . Either $C$ is critical and we are done, or we can drop a maximal event from $C$ to get a strictly smaller configuration $C^{\prime}$ satisfying $h(C^{\prime})=h(t)$ . Repeating this, we find a critical configuration $C$ of $t$ such that $h(C)=h(t)$ . By Lemma 5, the maximal events of $C$ are critical. Hence we get $C\subseteq{\downarrow}X_{t}$ . This implies $h({\downarrow}X_{t})\leq_{R}h(C)=h(t)$ . By $\mathcal{R}$ -triviality, we deduce $h({\downarrow}X_{t})=h(t)$ . $\hfill\blacktriangleleft$

The type of a trace $t=(E,\leq,\lambda)$ is the $\Sigma$ -labelled poset $\mathsf{type}(t)=(X_{t},\leq,\lambda)$ obtained as the restriction of the labelled poset $(E,\leq,\lambda)$ to the critical events of $t$ .

Example 8.

It is important to note that the type of a trace need not necessarily be a trace itself. Let $t=abc$ be a trace over the distributed alphabet $\Sigma_{1}=\{a,b\}$ , $\Sigma_{2}=\{b,c\}$ with 3 events $e_{1}<e_{2}<e_{3}$ labelled $a$ , $b$ , $c$ respectively, as shown in the figure below. Consider the $\mathcal{R}$ -trivial (commutative) monoid $M=(\{1,2,3\},\max,1)$ where $\max$ is the binary maximum operation. It is clear that $3<_{R}2<_{R}1$ . Consider the trace morphism $h\colon TR(\tilde{\Sigma})\to M$ defined by $h(a)=2$ , $h(b)=1$ and $h(c)=3$ . We see that only $e_{1}$ and $e_{3}$ are critical events of $t$ . Then, $\mathsf{type}(t)=(\{e_{1},e_{3}\},\leq,\lambda)$ with $e_{1}<e_{3}$ which is induced by the original partial order on $t$ . Since the labels $a$ and $c$ are independent, $\mathsf{type}(t)$ is not a trace.

Let $s=(Z,\leq,\lambda)$ be a $\Sigma$ -labelled poset. A linearization of $s$ is a word¹¹1A word $a_{1}a_{2}\cdots a_{n}\in\Sigma^{*}$ is identified with the structure $(\{e_{1},e_{2},\ldots,e_{n}\},\preceq,\lambda)$ with $\lambda(e_{i})=a_{i}$ and $e_{1}\prec e_{2}\prec\cdots\prec e_{n}$ . $w=(Z,\preceq,\lambda)$ where $\preceq$ is a total order on $Z$ which is consistent with $\leq$ , that is, satisfying ${\leq}\subseteq{\preceq}$ . We denote by $\mathsf{Lin}(s)\subseteq\Sigma^{*}$ the set of linearizations of $s$ .

Let $h^{\prime}\colon\Sigma^{*}\rightarrow M$ be the word morphism defined by $h^{\prime}(a)=h(a)$ for all $a\in\Sigma$ . For all traces $t\in TR(\tilde{\Sigma})$ and for all linearizations $w\in\mathsf{Lin}(t)$ , we have $h^{\prime}(w)=h(t)$ .

For every monoid element $m\in M$ we define $\Sigma^{m}=\{a\in\Sigma\mid m\cdot h(a)=m\}$ as the set of letters stabilizing $m$ . The complement $\Sigma\setminus\Sigma^{m}=\{a\in\Sigma\mid m\cdot h(a)\neq m\}$ also denoted $\overline{\Sigma^{m}}$ is the set of letters which cause an $\mathcal{R}$ -descent for $m$ . This means that for every $a\in\overline{\Sigma^{m}}$ $m\cdot h(a)<_{R}m$ .

Lemma 9.

Let $t=(E,\leq,\lambda)$ be a trace and $\mathsf{type}(t)=(X_{t},\leq,\lambda)$ be its type. For all linearizations $w\in\mathsf{Lin}(\mathsf{type}(t))$ , we have $h^{\prime}(w)=h(t)$ .

Proof.

The proof is by induction on the number $k=|X_{t}|$ of critical events of $t$ .

For the base case $k=0$ there are no critical events in $t$ . This means that $w=\varepsilon$ and all events in $t$ have labels in $\Sigma^{1_{M}}$ . Clearly, we have $h^{\prime}(\varepsilon)=1_{M}=h(t)$ .

Assume now $k>0$ and that the result holds for all traces $s$ with $|X_{s}|<k$ . Consider the linearization $w=a_{1}a_{2}\cdots a_{k}\in\mathsf{Lin}(\mathsf{type}(t))$ . We have $w=(X_{t},\preceq,\lambda)$ with $X_{t}=\{e_{1},e_{2},\ldots,e_{k}\}$ , $e_{1}\prec e_{2}\prec\cdots\prec e_{k}$ and $\lambda(e_{i})=a_{i}$ . Note that the event $e_{k}$ is maximal in ${\downarrow}X_{t}$ . Consider the trace $s$ which is the prefix of $t$ induced by $({\downarrow}X_{t})\setminus\{e_{k}\}$ . It is easy to see that $\mathsf{type}(s)=(\{e_{1},\ldots,e_{k-1}\},\leq,\lambda)$ and $v=a_{1}\cdots a_{k-1}\in\mathsf{Lin}(\mathsf{type}(s))$ . By induction, we have $h^{\prime}(v)=h(s)$ . Therefore, $h^{\prime}(w)=h^{\prime}(v)\cdot h^{\prime}(a_{k})=h(s)\cdot h(\lambda(e_{k}))% =h({\downarrow}X_{t})=h(t)$ where the last equality follows from Lemma 7. $\hfill\blacktriangleleft$

It follows immediately that the type of a trace determines its value under $h$ .

Corollary 10.

Let $t,t^{\prime}\in TR(\tilde{\Sigma})$ be two traces. If $\mathsf{type}(t)$ and $\mathsf{type}(t^{\prime})$ are isomorphic, denoted $\mathsf{type}(t)\cong\mathsf{type}(t^{\prime})$ , then $h(t)=h(t^{\prime})$ .

We conclude this subsection with some more definitions. Recall that we have fixed the distributed alphabet $\tilde{\Sigma}$ and the morphism $h$ from $TR(\tilde{\Sigma})$ to the finite $\mathcal{R}$ -trivial monoid $M$ . We define the type set of $\tilde{\Sigma}$ , with respect to $h$ , to be the set of all possible types of all traces over $\tilde{\Sigma}$ . More precisely, $\mathsf{types}(\tilde{\Sigma})=\{\mathsf{type}(t)\mid t\in TR(\tilde{\Sigma})\}$ . Note that, it clearly depends on $h$ . By Lemma 4, every type is a $\Sigma$ -labelled poset whose underlying set has size less than $|\mathscr{P}|\times|M|$ . Therefore $\mathsf{types}(\tilde{\Sigma})$ is a finite set.

By Corollary 10, the type of a trace determines its monoid value under the recognizing morphism $h$ . Hence we can define a function $\pi\colon\mathsf{types}(\tilde{\Sigma})\rightarrow M$ by $\pi(\mathsf{type}(t))=h(t)$ for all $t\in TR(\tilde{\Sigma})$ . Note that, by Lemma 9, if $\sigma=(X,\leq,\lambda)$ is a type then $\pi(\sigma)=h^{\prime}(w)$ for all $w\in\mathsf{Lin}(\sigma)$ .

Let $t=(E,\leq,\lambda)$ be a trace and $e\in E$ be an event. The type of $e$ in $t$ is the type of the prefix of $t$ induced by the strict past of $e$ : $\mathsf{type}(t,e)=\mathsf{type}({\Downarrow}e)=(X_{{\Downarrow}e},\leq,% \lambda)=(X_{t}\cap{\Downarrow}e,\leq,\lambda)$ . We have $\pi(\mathsf{type}(t,e))=h({\Downarrow}e)$ .

Lemma 11.

Let $t=(E,\leq,\lambda)$ be a trace and $e, f$ be events in $t$ . If $\mathsf{type}(t,e)=\mathsf{type}(t,f)=\sigma$ and $\lambda(e)=\lambda(f)\in\overline{\Sigma^{m}}$ where $m=\pi(\sigma)$ then $e=f$ .

Proof.

Assume towards a contradiction that there are two events $e, f$ in $t$ with $\mathsf{type}(t,e)=\mathsf{type}(t,f)=\sigma$ and $\lambda(e)=\lambda(f)=a\in\overline{\Sigma^{m}}$ where $m=\pi(\sigma)$ . Without loss of generality we may assume $e<f$ since they are both labelled with the same letter and hence are ordered. Then, $e$ is a critical event: indeed, $\mathsf{type}(t,e)=\sigma$ hence $h({\Downarrow}e)=\pi(\sigma)=m$ and $\lambda(e)=a\in\overline{\Sigma^{m}}$ implies that $h({\downarrow}e)=m\cdot h(a)\neq m$ . We deduce that $X_{{\Downarrow}e}\cup\{e\}\subseteq X_{{\Downarrow}f}$ : there are more critical events in the strict past of $f$ than in the strict past of $e$ . This is a contradiction with $\mathsf{type}(t,e)=\mathsf{type}(t,f)$ . $\hfill\blacktriangleleft$

3.3 Proof of Theorem 2 [ $1\to 2$ ]

Having done the necessary setup we now prove the first direction of Theorem 2 (restated as Theorem 14 at the end of this subsection). We start with Lemma 12 which supplies the key argument by constructing $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ event formulas for identifying the type of an event.

An event formula $\varphi$ of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ is called a strict past formula if it is a boolean combination of formulas of the form $\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi^{\prime}$ . A strict past formula does not test the label of the current event.

Lemma 12.

For every $\sigma\in\mathsf{types}(\tilde{\Sigma})$ , there exists a strict past event formula $\varphi_{\sigma}$ such that, for all traces $t=(E,\leq,\lambda)\in TR(\tilde{\Sigma})$ and all events $e$ in $t$ , $t,e\models\varphi_{\sigma}$ iff $\mathsf{type}(t,e)\cong\sigma$ .

Proof.

We construct $\varphi_{\sigma}$ by induction and prove that it has the correct property.
Base case: $|\sigma|=0$ , i.e., $\sigma=(\emptyset,\emptyset,\emptyset)$ . Note that $\pi((\emptyset,\emptyset,\emptyset))=1_{M}=h(\varepsilon)$ where $\varepsilon$ is the empty trace. We define $\varphi_{\sigma}=\mathop{\mathsf{YH}\vphantom{a}}\nolimits(\Sigma^{1_{M}})$ . We now prove that it has the desired property.

If $t,e\models\mathop{\mathsf{YH}\vphantom{a}}\nolimits(\Sigma^{1_{M}})$ then every letter in the strict past of $e$ stabilizes the monoid identity element. We deduce easily that there are no critical events in the strict past of $e$ . Therefore $\mathsf{type}(t,e)=(\emptyset,\emptyset,\emptyset)$ .

Conversely, if $\mathsf{type}(t,e)=(\emptyset,\emptyset,\emptyset)$ then there are no critical events in the strict past of $e$ . Since the empty trace is the smallest prefix of a trace and it maps to $1_{M}$ under $h$ , we deduce easily that every letter in the strict past of $e$ must stabilize the monoid identity $1_{M}$ . Therefore $t,e\models\mathop{\mathsf{YH}\vphantom{a}}\nolimits(\Sigma^{1_{M}})$ .
Induction hypothesis: Let $k\geq 0$ and assume that for every type $\sigma$ with $|\sigma|\leq k$ , we have constructed $\varphi_{\sigma}$ satisfying the property of the lemma. Consider an arbitrary type $\tau\in\mathsf{types}(\tilde{\Sigma})$ of size $k+1$ . We construct $\varphi_{\tau}$ below and prove its correctness.

Let $s=(E_{s},\leq_{s},\lambda_{s})\in TR(\tilde{\Sigma})$ be a trace with $\tau=\mathsf{type}(s)=(X_{s},\leq_{s},\lambda_{s})$ . For an element $x\in X_{s}$ , we let $\tau_{x}=({\Downarrow}_{\tau}x,\leq_{s},\lambda_{s})$ be the restriction of the labelled poset $\tau$ to the critical events strictly below $x$ ( ${\Downarrow}_{\tau}x=\{y\in X_{s}\mid y<_{s}x\}$ ). It is easy to see that $\tau_{x}=\mathsf{type}(s,x)=\mathsf{type}({\Downarrow}_{s}x)$ where ${\Downarrow}_{s}x=\{e\in E_{s}\mid e<_{s}x\}$ is (the prefix of $s$ induced by) the strict past of $x$ in $s$ . Let $m_{x}=h({\Downarrow}_{s}x)=\pi(\tau_{x})$ and $a_{x}=\lambda_{s}(x)$ . Since $x\in X_{s}$ is a critical event of $s$ , we have $h({\downarrow}_{s}x)=h({\Downarrow}_{s}x)\cdot h(\lambda_{s}(x))=m_{x}h(a_{x})% <_{R}m_{x}=h({\Downarrow}_{s}x)$ . Therefore, $a_{x}\in\overline{\Sigma^{m_{x}}}=\overline{\Sigma^{\pi(\tau_{x})}}$ .

Notice that the size of $\tau_{x}\in\mathsf{types}(\tilde{\Sigma})$ is at most $k$ . By induction hypothesis, we have a formula $\varphi_{\tau_{x}}$ satisfying the property of the lemma. We use the macro $\varphi(\tau,x)$ to denote the event formula $\varphi_{\tau_{x}}\land a_{x}$ . Finally, if $Z\subseteq X_{s}$ , we let $\tau_{Z}=({\downarrow}_{\tau}Z,\leq_{s},\lambda_{s})$ . Then, $\tau_{Z}=\mathsf{type}({\downarrow}_{s}Z)$ is a type and we let $m_{Z}=\pi(\tau_{Z})=h({\downarrow}_{s}Z)$ . We define

$\displaystyle\varphi_{\tau}$	$\displaystyle=\varphi_{1}\land\varphi_{2}\wedge\varphi_{order}$	$\displaystyle\varphi_{1}$	$\displaystyle=\mathop{\mathsf{YH}\vphantom{a}}\nolimits(\varphi_{crit}\lor% \varphi_{stab})$
$\displaystyle\varphi_{2}$	$\displaystyle=\bigwedge_{x\in X_{s}}\mathop{\mathsf{YP}\vphantom{a}}\nolimits% \varphi(\tau,x)$	$\displaystyle\varphi_{crit}$	$\displaystyle=\bigvee_{x\in X_{s}}\varphi(\tau,x)$
$\displaystyle\varphi_{order}$	$\displaystyle=\makebox[56.9055pt][l]{$\displaystyle\bigwedge_{x,y\in X_{s}\mid x% <_{s}y}\hskip-14.22636pt\mathop{\mathsf{YP}\vphantom{a}}\nolimits\Big{(}% \varphi(\tau,y)\wedge\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi(\tau,x)% \Big{)}\wedge\bigwedge_{x,y\in X_{s}\mid x\not<_{s}y}\hskip-14.22636pt\neg% \mathop{\mathsf{YP}\vphantom{a}}\nolimits\Big{(}\varphi(\tau,y)\wedge\mathop{% \mathsf{YP}\vphantom{a}}\nolimits\varphi(\tau,x)\Big{)}$}$
$\displaystyle\varphi_{stab}$	$\displaystyle=\makebox[56.9055pt][l]{$\displaystyle\bigvee_{Z={\downarrow}_{% \tau}Z\subseteq X_{s}}\Sigma^{m_{Z}}\wedge\bigwedge_{x\in Z}\mathop{\mathsf{YP% }\vphantom{a}}\nolimits\varphi(\tau,x)\land\bigwedge_{x\in X_{s}\setminus Z}% \lnot\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi(\tau,x)$}$

Before proceeding to the formal proof of correctness of $\varphi_{\tau}$ , we first provide an intuitive explanation of the various parts of $\varphi_{\tau}$ .

$\blacksquare$

$\varphi_{2}$ : asserts that for every “event” $x$ in $\tau$ , there is a (unique) corresponding critical event in the strict past whose type is isomorphic to $\tau_{x}$ and whose label is same as that of $x$ .
$\blacksquare$

$\varphi_{1}$ : asserts that every event in the strict past either corresponds to some “event” $x$ in $\tau$ (satisfies $\varphi_{crit}$ ) or is labelled with a stabilizing letter for the type $Z$ arising out of the “events” $x$ in $\tau$
$\blacksquare$

$\varphi_{order}$ : asserts that the ordering between “events” in $\tau$ and the corresponding critical events is identical.

We now formally show that $\varphi_{\tau}$ indeed satisfies the property of the lemma. Towards this, fix a trace $t=(E_{t},\leq_{t},\lambda_{t})$ and an event $e$ in $t$ .

( $\rightarrow$ ) Assume that $t,e\models\varphi_{\tau}$ . We show that $\mathsf{type}(t,e)\cong\tau$ .

First consider the fact that $t,e\models\varphi_{2}$ . This means that for all $x\in X_{s}$ , there exists an event $e_{x}\in{\Downarrow}_{t}e$ , such that $t,e_{x}\models\varphi(\tau,x)$ . By the inductive hypothesis, we have $\tau_{x}\cong\mathsf{type}(t,e_{x})=\mathsf{type}({\Downarrow}_{t}e_{x})$ and $\lambda_{t}(e_{x})=a_{x}\in\overline{\Sigma^{m_{x}}}$ . From Lemma 11, $e_{x}$ is the unique event in $t$ satisfying $\varphi(\tau,x)$ . Using $h({\Downarrow}_{t}e_{x})=\pi(\tau_{x})=m_{x}$ and $\lambda_{t}(e_{x})=a_{x}\in\overline{\Sigma^{m_{x}}}$ , we deduce that $e_{x}$ is critical in ${\Downarrow}_{t}e$ . Therefore, $Y=\{e_{x}\mid x\in X_{s}\}\subseteq X_{{\Downarrow}_{t}e}$ .

Now, using the fact that $t,e\models\varphi_{order}$ and the unicity of the events $e_{x}$ , we deduce that for all $x,y\in X_{s}$ , we have $x\leq_{s}y$ if and only if $e_{x}\leq_{t}e_{y}$ . We also know that for all $x\in X_{s}$ , we have $\lambda_{s}(x)=a_{x}=\lambda_{t}(e_{x})$ . Therefore, $\tau\cong(Y,\leq_{t},\lambda_{t})$ .

In order to obtain $\tau\cong\mathsf{type}(t,e)=(X_{{\Downarrow}_{t}e},\leq_{t},\lambda_{t})$ as desired, it remains to prove that $Y=X_{{\Downarrow}_{t}e}$ . Towards a contradiction, assume that this is not the case and consider a minimal event $f\in X_{{\Downarrow}_{t}e}\setminus Y$ . Since $t,e\models\varphi_{1}$ , we have $t,f\models\varphi_{crit}\lor\varphi_{stab}$ . If $t,f\models\varphi_{crit}$ then $t,f\models\varphi(\tau,x)$ for some $x\in X_{s}$ and by the unicity constraint $f=e_{x}\in Y$ , a contradiction. Hence, $t,f\models\varphi_{stab}$ and there is a downward closed set $Z={\downarrow}_{\tau}Z\subseteq X_{s}$ such that $\lambda_{t}(f)\in\Sigma^{m_{Z}}$ and ${\Downarrow}_{t}f\cap Y=\{e_{x}\mid x\in Z\}$ . By minimality of $f$ , we get ${\Downarrow}_{t}f\cap X_{{\Downarrow}_{t}e}={\Downarrow}_{t}f\cap Y=\{e_{x}% \mid x\in Z\}$ . We deduce that $\mathsf{type}(t,f)=(\{e_{x}\mid x\in Z\},\leq_{t},\lambda_{t})\cong\tau_{Z}$ and $h({\Downarrow}_{t}f)=m_{Z}$ . Using $\lambda_{t}(f)\in\Sigma^{m_{Z}}$ we conclude that $f$ is not critical, a contradiction.

( $\leftarrow$ ) Conversely, assume that $\tau\cong\mathsf{type}(t,e)$ . We show that $t,e\models\varphi_{\tau}$ .

From the isomorphism between $\tau=(X_{s},\leq_{s},\lambda_{s})$ and $\mathsf{type}(t,e)=(X_{{\Downarrow}_{t}e},\leq_{t},\lambda_{t})$ we get a one-one correspondence $x\in X_{s}\mapsto e_{x}\in X_{{\Downarrow}_{t}e}$ such that for all $x,y\in X_{s}$ we have $x\leq_{s}y$ if and only if $e_{x}\leq_{t}e_{y}$ and $\lambda_{t}(e_{x})=\lambda_{s}(x)$ . We deduce that $\mathsf{type}(t,e_{x})\cong\tau_{x}$ and $\lambda_{t}(e_{x})=a_{x}$ for all $x\in X_{s}$ . Therefore, $t,e_{x}\models\varphi(\tau,x)$ for all $x\in X_{s}$ and $t,e\models\varphi_{2}$ .

Next, it is easy to check that $t,e\models\varphi_{order}$ using the unicity property (Lemma 11) and the fact that $x<_{s}y$ if and only if $e_{x}<_{t}e_{y}$ for all $x,y\in X_{s}$ .

Let $f\in{\Downarrow}_{t}e$ be an event in the strict past of $e$ . Either $f\in X_{{\Downarrow}_{t}e}$ is a critical event and $f=e_{x}$ for some $x\in X_{s}$ . In this case, we get $t,f\models\varphi(\tau,x)$ and $t,f\models\varphi_{crit}$ . Or $f\in{\Downarrow}_{t}e\setminus X_{{\Downarrow}_{t}e}$ is a non-critical event. Let $Z=\{x\in X_{s}\mid e_{x}<f\}$ . Then, $Z={\downarrow}_{\tau}Z$ is downward closed and using the unicity property we deduce that $t,f\models\bigwedge_{x\in Z}\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi(% \tau,x)\land\bigwedge_{x\in X_{s}\setminus Z}\lnot\mathop{\mathsf{YP}\vphantom% {a}}\nolimits\varphi(\tau,x)$ . Now, due to the fact that $\tau\cong\mathsf{type}(t,e)$ it is clear that $\tau_{Z}\cong\mathsf{type}(t,f)$ . We deduce that $m_{Z}=\pi(\tau_{Z})=h({\Downarrow}_{t}f)$ . Since $f$ is not critical, we have $\lambda_{t}(f)\in\Sigma^{m_{Z}}$ . Therefore, $t,f\models\varphi_{stab}$ . We have shown that $t,e\models\varphi_{1}$ . $\hfill\blacktriangleleft$

Lemma 13.

For every element $m\in M$ we can define a strict past event formula $\varphi_{m}$ in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ such that for every trace $t$ and event $e$ of $t$ , we have $t,e\models\varphi_{m}\text{ iff }h({\Downarrow}e)=m$ .

Proof.

We define $\varphi_{m}=\bigvee_{\sigma\in\mathsf{types}(\tilde{\Sigma}):\pi(\sigma)=m}% \varphi_{\sigma}$ and show that it has the desired property.

Let $t$ be a trace and $e$ be an event in $t$ . If $t,e\models\varphi_{m}$ then there exists some $\sigma\in\mathsf{types}(\tilde{\Sigma})$ such that $\pi(\sigma)=m$ and $t,e\models\varphi_{\sigma}$ . By Lemma 12, $\sigma\cong\mathsf{type}(t,e)=\mathsf{type}({\Downarrow}e)$ . By definition of $\pi$ , we have $h({\Downarrow}e)=\pi(\sigma)$ . As $\pi(\sigma)=m$ , we conclude that $h({\Downarrow}e)=m$ . Now for the other direction assume $h({\Downarrow}e)=m$ . By Lemma 12, $t,e\models\varphi_{\mathsf{type}(t,e)}$ and by definition of $\pi$ , $\pi(\mathsf{type}(t,e))=h({\Downarrow}e)$ . As $h({\Downarrow}e)=m$ , $\pi(\mathsf{type}(t,e))=m$ and hence $t,e\models\varphi_{m}$ . $\hfill\blacktriangleleft$

Theorem 14.

Let $L\subseteq TR(\tilde{\Sigma})$ be recognized by the morphism $h:TR(\tilde{\Sigma})\to M$ . Then there is a sentence $\Phi_{L}$ of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ which defines $L$ : for all traces $t\in TR(\tilde{\Sigma})$ , $t\models\Phi_{L}\iff t\in L$ .

Proof.

As $L$ is recognized by $h$ , there is a subset $P\subseteq M$ such that $L=h^{-1}(P)$ . For each monoid element $m\in M$ , we define below a sentence $\Phi_{m}$ of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ which defines the trace language $h^{-1}(m)$ : for all traces $t$ we have $t\models\Phi_{m}\iff h(t)=m$ . The sentence defining $L$ is $\Phi_{L}=\bigvee_{m\in P}\Phi_{m}$ .

Let $\#\notin\Sigma$ be a new letter. We extend the distributed alphabet $\tilde{\Sigma}$ by making $\#$ an action shared by all processes: $\tilde{\Sigma}_{\#}=\{\Sigma_{i}\cup\{\#\}\}_{i\in\mathscr{P}}$ . For each trace $t\in TR(\tilde{\Sigma})$ , we consider the augmented trace $\bar{t}=t\cdot\#\in TR(\tilde{\Sigma}_{\#})$ obtained by adding a maximum event $e_{\#}$ labelled $\#$ to $t$ . Note that all processes participate in $e_{\#}$ and $t={\Downarrow}e_{\#}$ . Now by Lemma 13, we have a strict past event formula²²2Formally the formula $\varphi_{m}$ may use $\#$ . We can take care of this by using $\lnot\Sigma$ wherever it occurs in the formula. $\varphi_{m}$ , such that $\bar{t},e_{\#}\models\varphi_{m}\iff h({\Downarrow}e_{\#})=m\iff h(t)=m$ . We can now set $\Phi_{m}$ as the sentence obtained by replacing every outermost occurrence of $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ in $\varphi_{m}$ by $\mathop{\mathsf{E}\vphantom{a}}\nolimits$ . It is easy to see that $t\models\Phi_{m}$ iff $\bar{t},e_{\#}\models\varphi_{m}$ . As a result, $t\models\Phi_{m}$ iff $h(t)=m$ . $\hfill\blacktriangleleft$

4 Logic to cascade products to algebra

In this section, we first introduce a localized version of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ namely $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ and show that both have the same expressive power. $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ is more suited for the direction $2\to 3$ of Theorem 2 where we connect logic to cascade products of asynchronous automata. Subsequently, in Section 4.2 we introduce asynchronous devices and their cascade products and prove Theorem 22 in Section 4.3. Finally we show the $3\to 1$ direction of Theorem 2 by connecting cascade products to algebra in Theorem 24.

4.1 $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ and its equivalence with $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$

We define local modalities $\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}$ and $\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}$ for each process $i\in\mathscr{P}$ as follows:

\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi=\mathop{\mathsf{E}% \vphantom{a}}\nolimits(\Sigma_{i}\wedge\varphi)\mbox{\leavevmode\nobreak\ % \leavevmode\nobreak\ and\leavevmode\nobreak\ \leavevmode\nobreak\ }\mathop{% \mathsf{YP}\vphantom{a}}\nolimits_{i}\varphi=\Sigma_{i}\wedge\mathop{\mathsf{% YP}\vphantom{a}}\nolimits(\Sigma_{i}\wedge\varphi)

Let $t$ be a trace and $e$ be an event of $t$ . It is clear that, $t,e\models\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}\varphi$ iff $e$ is an $i$ -event and there exists an $i$ -event $e^{\prime}$ in the strict past of $e$ such that $t,e^{\prime}\models\varphi$ . Further $t\models\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi$ iff there exists an $i$ -event $f$ of $t$ such that $t,f\models\varphi$ .

We define $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ as a fragment of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ in which only above local modalities are allowed. More precisely, the syntax of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ logic is as follows:

	$\displaystyle\Phi$	$\displaystyle::=\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi\mid\Phi_{1% }\lor\Phi_{2}\mid\lnot\Phi$
	$\displaystyle\varphi$	$\displaystyle::=a\mid\varphi_{1}\lor\varphi_{2}\mid\lnot\varphi\mid\mathop{% \mathsf{YP}\vphantom{a}}\nolimits_{i}\varphi$

Lemma 15.

$\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ and $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ express the same class of trace languages over $\tilde{\Sigma}$ .

Proof.

We only need to show how to express the modalities $\mathop{\mathsf{E}\vphantom{a}}\nolimits$ and $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ with the local modalities of $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ . We have $\mathop{\mathsf{E}\vphantom{a}}\nolimits\varphi=\bigvee_{i\in\mathscr{P}}% \mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi$ .

For the strict past modality $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ we use a well-known fact on traces. Let $t=(E,\leq,\lambda)$ be a trace and $e, f$ be events in $t$ . Then $e<f$ if and only if there is a sequence of events $e=e_{0}<e_{1}<e_{2}<\cdots<e_{k}=f$ with $1\leq k\leq|\mathscr{P}|$ and for each $1\leq j\leq k$ , there is a process $i_{j}\in\mathscr{P}$ such that $e_{j-1},e_{j}$ are both $i_{j}$ -events. It is easy to deduce from here that

\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi=\bigvee_{\begin{subarray}{c}i% _{1},i_{2},\ldots,i_{k}\in\mathscr{P}\\ 1\leq k\leq|\mathscr{P}|\end{subarray}}\mathop{\mathsf{YP}\vphantom{a}}% \nolimits_{i_{k}}\cdots\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i_{2}}% \mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i_{1}}\varphi\,.

This shows that $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ modality can be expressed in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ and concludes the proof. $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 16.

Referring to the syntax and semantics from [1] (Section 2.2), it is clear that $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ is a sublogic of $\mathsf{LocPastPDL}$ . Indeed, let $\varphi$ be a $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ event formula and assume there exists an equivalent event formula $\overline{\varphi}$ in $\mathsf{LocPastPDL}$ . Then $\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}\varphi$ is implemented with $\langle{\leftarrow_{i}^{+}}\rangle\overline{\varphi}$ and $\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi$ is implemented with $\mathop{\mathsf{EM}\vphantom{a}}\nolimits_{i}(\langle{\leftarrow_{i}^{*}}% \rangle\overline{\varphi})$

4.2 Asynchronous devices and cascade product

We now recall the model of asynchronous automata due to Zielonka [23].

A deterministic asynchronous automaton $A$ over $\tilde{\Sigma}$ (or simply over $\Sigma$ ) is a tuple $A=({\{S_{i}\}}_{i\in\mathscr{P}},{\{\delta_{a}\}}_{a\in\Sigma},{s}_{\mathrm{in% }})$ where

$\blacksquare$

for each $i\in\mathscr{P}$ , $S_{i}$ is a finite non-empty set of local $i$ -states.
$\blacksquare$

for each $a\in\Sigma$ , $\delta_{a}\colon S_{a}\to S_{a}$ is a deterministic joint transition function where $S_{a}=\prod_{i\in\mathsf{loc}(a)}S_{i}$ is the set of $a$ -states.
$\blacksquare$

with $S=\prod_{i\in\mathscr{P}}S_{i}$ as the set of all global states, ${s}_{\mathrm{in}}\in S$ is a designated initial global state.

Let $s\in S$ be a global state. We can write $s$ as $(s_{a},s_{-a})$ where $s_{a}$ is the projection of $s$ onto $\mathsf{loc}(a)$ and $s_{-a}$ is the projection onto $\mathscr{P}\setminus\mathsf{loc}(a)$ . For any letter $a\in\Sigma$ , we can extend the joint transition function $\delta_{a}\colon S_{a}\to S_{a}$ to a global transition function $\Delta_{a}\colon S\to S$ on global states as follows: $\Delta_{a}((s_{a},s_{-a}))=(\delta_{a}(s_{a}),s_{-a})$ . For a trace $t\in TR(\tilde{\Sigma})$ , we let $\Delta_{\varepsilon}$ be the identity function on $S$ , and define $\Delta_{t}\colon S\to S$ as the composition $\Delta_{t}=\Delta_{a}\circ\Delta_{t^{\prime}}$ when $t=t^{\prime}a$ . Note that $\Delta_{t}$ is well defined, since for any pair $(a,b)$ of independent letters, $\Delta_{a}\circ\Delta_{b}=\Delta_{b}\circ\Delta_{a}$ . We denote by $A(t)$ the global state $\Delta_{t}({s}_{\mathrm{in}})$ reached when $A$ runs on $t$ .

At this point we define the transition monoid $M(A)$ associated with the asynchronous automaton $A$ . Let $M(A)$ be the finite set of functions $\{\Delta_{t}\mid t\in TR(\tilde{\Sigma})\}$ . This set under the usual function composition operation is a monoid with $\Delta_{\varepsilon}$ as it’s identity element.

For any asynchronous automaton $A$ , if we fix some $F\subseteq S$ to be the set of accepting global states then we say $L(A,F)=\{t\mid A(t)\in F\}$ is the trace language accepted by $A$ .

We also use asynchronous automata as letter-to-letter asynchronous transducers as in [19, 2, 3] which compute a relabelling function. Let $\Gamma$ be a finite non-empty set. We can define a natural extended distributed alphabet, $\widetilde{\Sigma\times\Gamma}$ by inheriting the distribution from $\tilde{\Sigma}$ that is, $\mathsf{loc}((a,\gamma))=\mathsf{loc}(a)$ . $TR(\tilde{\Sigma})$ and $TR(\widetilde{\Sigma\times\Gamma})$ are the set of traces over the original and extended distributed alphabets. A function $\theta\colon TR(\tilde{\Sigma})\to TR(\widetilde{\Sigma\times\Gamma})$ is called a $\Gamma$ -labelling function if, for every $t=(E,\leq,\lambda)\in TR(\tilde{\Sigma})$ , $\theta(t)=(E,\leq,(\lambda,\mu))\in TR(\widetilde{\Sigma\times\Gamma})$ . A $\Gamma$ -labelling function decorates each event $e$ of the trace $t$ with a label $\mu(e)$ from $\Gamma$ .

An asynchronous $\Gamma$ -transducer over $\tilde{\Sigma}$ (or simply $\Sigma$ ) is a tuple $\widehat{A}=(A,\{\mu_{a}\})$ where $A=(\{S_{i}\},\{\delta_{a}\},{s}_{\mathrm{in}})$ is an asynchronous automaton and each $\mu_{a}$ ( $a\in\Sigma$ ) is a map $\mu_{a}\colon S_{a}\to\Gamma$ . We overload notation and use $\widehat{A}\colon TR(\tilde{\Sigma})\to TR(\widetilde{\Sigma\times\Gamma})$ to also denote the $\Gamma$ -labelling function computed by the transducer $\widehat{A}$ . For $t=(E,\leq,\lambda)\in TR(\tilde{\Sigma})$ , we define $\widehat{A}(t)=(E,\leq,(\lambda,\mu))\in TR(\widetilde{\Sigma\times\Gamma})$ such that, for every $e\in E$ with $\lambda(e)=a$ , $\mu(e)=\mu_{a}(s_{a})$ where $s=A({\Downarrow}e)$ .

An asynchronous automaton (resp. transducer) with local state sets $\{S_{i}\}$ is said to be localized at process $i$ if all local state sets $S_{j}$ with $j\neq i$ are singletons. It is localized if it is localized at some process. For an automaton/transducer localized at $i$ , all non-trivial transitions are on letters in which process $i$ participates.

Figure 1:

U_{1}[i]

automaton.

Example 17.

We define $U_{1}[i]$ to be a deterministic asynchronous automaton which is localized at process $i$ . In $U_{1}[i]$ , the local state set of process $i$ has two states: $S_{i}=\{1,2\}$ while all other processes have a single state. In Figure 1 we show the local automaton for process $i$ , which operates only on $\Sigma_{i}=\Sigma_{i_{1}}\uplus\Sigma_{i_{2}}$ . Note that, a letter in $\Sigma_{i_{2}}$ allows to change the local state from $1$ to $2$ while the rest of the transitions are self-loops. Clearly, we can identify the global-states of $U_{1}[i]$ with $S_{i}$ . With this convention, we always use $1$ as the initial global state for $U_{1}[i]$ . Note that the transition monoid of $U_{1}[i]$ is isomorphic to a submonoid of $U_{1}$ from Example 1. For a trace $t$ , $U_{1}[i](t)$ , the global state reached by $U_{1}[i]$ when run on $t$ , is $2$ iff there exists an $i$ -event in $t$ with label in $\Sigma_{i_{2}}$ .

A degenerate $U_{1}[i]$ automaton is a $U_{1}[i]$ automaton for which $\Sigma_{i_{2}}=\emptyset$ . As state $2$ is not reachable from the initial state $1$ , we can safely assume that $S_{i}=\{1\}$ . Observe that the transition monoid of a degenerate $U_{1}[i]$ is the trivial monoid.

Example 18.

An asynchronous $\Gamma$ -transducer over $\Sigma$ whose underlying automaton is $U_{1}[i]$ from Example 17, is denoted by $\widehat{U_{1}[i]}$ . More precisely, $\widehat{U_{1}[i]}=(U_{1}[i],\{\mu_{a}\})$ . Recall that in $U_{1}[i]$ , $S_{i}=\{1,2\}$ and $S_{j}=\{1\}$ for $j\neq i$ . Further, for each $a\in\Sigma$ , $\mu_{a}\colon S_{a}\to\Gamma$ . These output functions $\{\mu_{a}\}$ can be viewed as follows.

1.

For each $a$ such that $i\in\mathsf{loc}(a)$ , we identify $S_{a}$ with $S_{i}$ . Thus, $\mu_{a}\colon S_{i}\to\Gamma$ .
2.

For each $a$ such that $i\not\in\mathsf{loc}(a)$ , $S_{a}$ is a singleton. As a result, $\mu_{a}$ is a constant function and can be simply thought of as an element of $\Gamma$ .

Note that, $\widehat{U_{1}[i]}$ always uses $1$ as the initial global state and it has an associated $\Gamma$ -labelling function $\widehat{U_{1}[i]}\colon TR(\tilde{\Sigma})\to TR(\widetilde{\Sigma\times% \Gamma})$ .

A degenerate $\widehat{U_{1}[i]}$ $\Gamma$ -transducer has a degenerate $U_{1}[i]$ as its underlying automaton and has effectively only one global state. As a result, its output function can be simply specified as a output function $\mu\colon\Sigma\to\Gamma$ .

Now we introduce the local cascade product of asynchronous transducers [4, 3] which will play an important role in later sections.

Definition 19.

Let $\widehat{A}=(\{S_{i}\},\{\delta_{a}\},{s}_{\mathrm{in}},\{\mu_{a}\})$ be a $\Gamma$ -transducer over $\Sigma$ and $\widehat{B}=(\{Q_{i}\},\{\delta_{(a,\gamma)}\},{q}_{\mathrm{in}},\{\nu_{(a,% \gamma)}\})$ be $\Pi$ -transducer over $\Sigma\times\Gamma$ . We define the local cascade product of $\widehat{A}$ and $\widehat{B}$ to be the $\Pi$ -transducer $\widehat{A}\circ_{\ell}\widehat{B}=(\{S_{i}\times Q_{i}\},\{\nabla_{a}\},({s}_% {\mathrm{in}},{q}_{\mathrm{in}}),\{\tau_{a}\})$ over $\Sigma$ where $\nabla_{a}((s_{a},q_{a}))=(\delta_{a}(s_{a}),\delta_{(a,\mu_{a}(s_{a}))}(q_{a}))$ and $\tau_{a}\colon S_{a}\times Q_{a}\to\Pi$ is defined by $\tau_{a}((s_{a},q_{a}))=\nu_{(a,\mu_{a}(s_{a}))}(q_{a})$ .

In the sequential case, that is, when $|\mathscr{P}|=1$ , the local cascade product coincides with the well-known operation of cascade product of sequential letter-to-letter transducers.

The following lemma is easily verified. See [3] for more details.

Lemma 20.

The $\Pi$ -labelling function computed by $\widehat{A}\circ_{\ell}\widehat{B}$ is the composition of the $\Gamma$ -labelling function computed by $\widehat{A}$ and the $\Pi$ -labelling function computed by $\widehat{B}$ : for every $t\in TR(\tilde{\Sigma})$ ,

(\widehat{A}\circ_{\ell}\widehat{B})(t)=\widehat{B}(\widehat{A}(t))

Although we have defined the local cascade product of transducers, it is equally easy to define the local cascade product of asynchronous automata. We refer to [3] for precise details of this construction and its connection with the wreath product operation and the resulting local cascade product principle.

4.3 Proof of Theorem 2 [ $2\to 3$ ]

In this section, we provide a proof of $2\to 3$ of Theorem 2. In view of Lemma 15, it suffices to show that languages expressed by $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ sentences are accepted by local cascade product of $U_{1}[i]$ automata. This is precisely the content of Theorem 22.

Let $\varphi$ be a $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ event formula. For each trace $t\in TR(\tilde{\Sigma})$ and event $e$ in $t$ , we let $\mu_{\varphi}(e)\in\{\top,\bot\}$ be the truth value of $\varphi$ at $e$ , and we let $\theta^{\varphi}$ be the $\{\top,\bot\}$ -labelling function given by $\theta^{\varphi}(t)=(E,\leq,(\lambda,\mu_{\varphi}))$ , for each $t=(E,\leq,\lambda)\in TR(\tilde{\Sigma})$ .

Lemma 21.

Let $\varphi$ be a $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ event formula and let $\theta^{\varphi}$ be the corresponding $\{\top,\bot\}$ -labelling function. Then we can construct a local cascade product $\widehat{A}_{\varphi}$ of $\widehat{U_{1}[i]}$ transducers which computes $\theta^{\varphi}$ .

Proof.

The construction of $\widehat{A}_{\varphi}$ proceeds by structural induction on $\varphi$ . We first consider the base case with $\varphi=a$ . Fix some process $i\in\mathsf{loc}(a)$ . We let $\widehat{A}_{\varphi}$ be the degenerate $\{\top,\bot\}$ -transducer $\widehat{U_{1}[i]}$ over $\Sigma$ whose output function is $\mu\colon\Sigma\to\{\top,\bot\}$ where $\mu(b)=\top$ if $b=a$ and $\mu(b)=\bot$ otherwise. Clearly, the $\{\top,\bot\}$ -labelling function computed by $\widehat{A}_{\varphi}$ coincides with $\theta^{\varphi}$ .

Now we consider the inductive case where $\varphi=\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}\varphi^{\prime}$ . By induction, we have $\{\top,\bot\}$ -transducer $\widehat{A}_{\varphi^{\prime}}$ which computes $\theta^{\varphi^{\prime}}$ . Note that the output alphabet of $\widehat{A}_{\varphi^{\prime}}$ is $\Pi=\Sigma\times\{\top,\bot\}$ with the distribution $\Pi_{i}=\Sigma_{i}\times\{\top,\bot\}$ .

We construct $\widehat{A}_{\varphi}$ as a local cascade product $\widehat{A}_{\varphi^{\prime}}\circ_{\ell}\widehat{B}$ , where $\widehat{B}$ is a $\{\top,\bot\}$ -transducer $\widehat{U_{1}[i]}$ over $\Pi$ defined below, so that $\widehat{A}_{\varphi}$ computes $\theta^{\varphi}$ . In view of Lemma 20, $\widehat{A}_{\varphi}(t)=\widehat{B}(\widehat{A}_{\varphi^{\prime}}(t))$ . By induction on $\varphi^{\prime}$ , $\widehat{A}_{\varphi^{\prime}}=\theta^{\varphi^{\prime}}$ . Thus, the requirement that $\widehat{A}_{\varphi}$ computes $\theta^{\varphi}$ simply translates to the requirement that $\widehat{B}(\theta^{\varphi^{\prime}}(t))=\theta^{\varphi}(t)$ .

Let $t=(E,\leq,\lambda)$ be a trace over $\Sigma$ and $t^{\prime}=\theta^{\varphi^{\prime}}(t)=(E,\leq,(\lambda,\mu^{\prime}))$ . Further, let $t^{\prime\prime}=\theta^{\varphi}(t)=(E,\leq,(\lambda,\mu))$ . As $\varphi=\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}\varphi^{\prime}$ , for an event $e\in E$ , $\mu(e)=\top$ iff $e$ is an $i$ -event and there is an $i$ -event $f$ in the strict past of $e$ such that $\mu^{\prime}(f)=\top$ .

We are now ready to construct $\widehat{B}$ as a $\widehat{U_{1}[i]}$ transducer over $\Pi$ so as $\widehat{B}(t^{\prime})=t^{\prime\prime}$ . The local component for process $i$ in $\widehat{B}=\widehat{U_{1}[i]}$ is as depicted in the figure below.

More precisely, for $\widehat{B}$ over $\Pi$ , with $S_{i}=\{1,2\}$ , the only non-self-loop transitions (from local state $1$ to local state $2$ ) are on letters of the form $(a,\top)$ with $a\in\Sigma_{i}$ . The output functions are as follows. For $a\in\Sigma_{i}$ , $\mu_{(a,*)}(1)=\bot$ , $\mu_{(a,*)}(2)=\top$ and for $a\not\in\Sigma_{i}$ , $\mu_{(a,*)}=\bot$ .

Clearly, $\widehat{B}$ outputs $\bot$ on events in which process $i$ does not participate. Further, it outputs $\top$ on an $i$ -event only after reaching state $2$ which ensures that there is an $i$ -event in the strict past where the input label (the truth value of $\varphi^{\prime}$ ) carries the value $\top$ . It is easy to see from here that, for every $t\in TR(\tilde{\Sigma})$ , $\widehat{B}(\theta^{\varphi^{\prime}}(t))=\theta^{\varphi}(t)$ . This in turn implies that $\widehat{A}_{\varphi}=\widehat{A}_{\varphi^{\prime}}\circ_{\ell}\widehat{B}$ correctly computes $\theta^{\varphi}$ .

We now consider the case where $\varphi=\varphi_{1}\lor\varphi_{2}$ . By induction, we have a transducer $\widehat{A}_{\varphi_{1}}$ ( $\widehat{A}_{\varphi_{2}}$ ) which computes $\theta^{\varphi_{1}}$ (respectively $\theta^{\varphi_{2}}$ ). We consider the natural direct product $\widehat{A}=\widehat{A}_{\varphi_{1}}\times\widehat{A}_{\varphi_{2}}$ which is a $(\{\top,\bot\}\times\{\top,\bot\})$ -transducer which simultaneously computes the truth values of $\varphi_{1}$ as well as $\varphi_{2}$ . We can easily see that the direct product is a special case of the cascade product. We can simply define $\widehat{A}_{\varphi}=\widehat{A}\circ_{\ell}\widehat{B}$ where $\widehat{B}$ is a degenerate $\{\top,\bot\}$ -transducer $\widehat{U_{1}[i]}$ (for any process $i$ ) over $\Sigma\times(\{\top,\bot\}\times\{\top,\bot\})$ whose output function $\mu$ is as follows: $\mu((a,b_{1},b_{2}))=b_{1}\lor b_{2}$ . It is easy to see that $\widehat{A}$ computes $\theta^{\varphi}$ .

The remaining case where $\varphi=\lnot\varphi^{\prime}$ can be similarly handled by a local cascade product of $\widehat{A}_{\varphi^{\prime}}$ with a degenerate $\widehat{U_{1}[i]}$ transducer. $\hfill\blacktriangleleft$

Theorem 22.

Let $\Phi$ be a $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ sentence. There exists an asynchronous automaton $A_{\Phi}$ which is a cascade product of $U_{1}[i]$ automata and it accepts exactly the trace language defined by $\Phi$ . In other words, $A_{\Phi}$ accepts $L_{\Phi}=\{t\in TR(\tilde{\Sigma})\mid t\models\Phi\}$ .

Proof.

A basic $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ trace formula $\Phi$ is of the form $\mathop{\mathsf{E}\vphantom{a}}\nolimits_{j}\varphi$ , where $\varphi$ is a $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ event formula. For a trace $t$ , we have that $t\models\mathop{\mathsf{E}\vphantom{a}}\nolimits_{j}\varphi$ iff there exists a $j$ -event $e$ in the trace such that $t,e\models\varphi$ . From Lemma 21 we have a $\{\top,\bot\}$ -transducer $\widehat{A}_{\varphi}$ which is a local cascade product of $\widehat{U_{1}[i]}$ transducers such that $\widehat{A}_{\varphi}=\theta^{\varphi}$ . Let $t=(E,\leq,\lambda)$ be any trace over $\Sigma$ . It is clear that $t\models\mathop{\mathsf{E}\vphantom{a}}\nolimits_{j}\varphi$ iff some $j$ -event in the output trace $t^{\prime}=\widehat{A}_{\varphi}(t)$ is labelled by $\top$ . Therefore the desired property of $A_{\Phi}$ is that it should accept the trace $t$ iff $t^{\prime}$ has a $\top$ -labelled $j$ -event. To achieve this, we simply take the cascade product of the $\{\top,\bot\}$ -transducer $\widehat{A}_{\varphi}$ with an asynchronous automaton $U_{1}[j]$ over $\Sigma\times\{\top,\bot\}$ . Beginning in the initial global state $1$ , the non-trivial component of $U_{1}[j]$ automaton owned by process $j$ waits at local state $1$ for the label $\top$ to occur on $j$ -events and transits to local state $2$ after seeing the label $\top$ and stays there thereafter. This $U_{1}[j]$ automaton is depicted in the figure below.

In order to accept $L_{\Phi}$ , in the automaton $A_{\Phi}=\widehat{A}_{\varphi}\circ_{\ell}U_{1}[j]$ , we define a global state of $A_{\Phi}$ to be accepting if its component for the last (in the cascade product) $U_{1}[j]$ global state is $2$ . As $\widehat{A}_{\varphi}$ is a local cascade product of $\widehat{U_{1}[i]}$ transducers and the underlying automaton for each $\widehat{U_{1}[i]}$ is simply a $U_{1}[i]$ automaton, it is not difficult to see that $A_{\Phi}$ is in fact a local cascade product of $U_{1}[i]$ automata.

This takes care of basic primitive languages defined by sentences of the form $\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi$ . As a general sentence $\Phi$ is a boolean combination of sentences of the form $\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}\varphi$ , $L_{\Phi}$ is also a boolean combination of basic primitive languages. The result for general $\Phi$ follows as boolean combinations can be handled by direct product construction which can be easily implemented by the local cascade product construction. $\hfill\blacktriangleleft$

4.4 Proof of Theorem 2 [ $3\to 1$ ]

In this subsection, we provide a proof of $3\to 1$ of Theorem 2 in the form of Theorem 24.

Lemma 23.

Let $A$ be an asynchronous automaton over $\Sigma$ which is a local cascade product of $U_{1}[i]$ automata. Then the transition monoid of $A$ is $\mathcal{R}$ -trivial.

Proof.

Let $A=(\{S_{i}\},\{\delta_{a}\},s_{in})$ be a local cascade product of $U_{1}[i]$ automata. We show that there is a partial order $\leq$ on the global state set $S=\prod_{i\in\mathscr{P}}S_{i}$ such that, for every $(s,a)\in S\times\Sigma$ , $\Delta_{a}(s)\leq s$ (recall that, $\Delta_{a}\colon S\to S$ is the natural global transition function induced by the joint transition function $\delta_{a}\colon S_{a}\to S_{a}$ ). It is known [6] and easy to see that the existence of such a partial order implies that the transition monoid of $A$ is $\mathcal{R}$ -trivial.

We show the existence of the required partial order by induction on the number of constituent $U_{1}[i]$ automata in $A$ . In the base case, $A$ itself is a $U_{1}[i]$ . As the global state set of $U_{1}[i]$ is $\{1,2\}$ (see Example 17), by setting $\leq$ to be the total order with $2<1$ , we get the desired property.

To complete the inductive step, we assume the existence of a partial order $\preceq$ on the global state set $S$ of $A$ . We now use it to construct the required partial order $\leq$ on the global state set of $A\circ_{\ell}U_{1}[i]$ . Note that the global state set of $A\circ_{\ell}U_{1}[i]$ is simply $S\times\{1,2\}$ . We define $\leq$ as follows: for $s,s^{\prime}\in S$ and $k,k^{\prime}\in\{1,2\}$ , $(s^{\prime},k^{\prime})\leq(s,k)$ iff $s^{\prime}\preceq s$ , and $k^{\prime}\leq k$ . In other words, $\leq$ is simply the direct product of $\preceq$ on $S$ and the total order on $\{1,2\}$ with $2<1$ . Let $a\in\Sigma$ , then the (global) deterministic transition on $a$ of $A\circ_{\ell}U_{1}[i]$ takes the state $(s,k)$ to the state $(s^{\prime},k^{\prime})=(\Delta_{a}(s),\Delta_{(a,s_{a})}(k))$ . It is clear from this description that $(s^{\prime},k^{\prime})\leq(s,k)$ . This shows that $\leq$ on $S\times\{1,2\}$ has the desired property and we are done. $\hfill\blacktriangleleft$

Theorem 24.

Let $L\subseteq TR(\tilde{\Sigma})$ be accepted by an asynchronous automaton $A$ which is a local cascade product of $U_{1}[i]$ automata. Then $L$ is $\mathcal{R}$ -trivial.

Proof.

We consider the transition monoid $M(A)$ associated with $A$ . Recall that it is the finite monoid consisting of $\{\Delta_{t}\colon t\in TR(\tilde{\Sigma})\}$ where $\Delta_{t}$ is the global transition function on the global state set induced by the trace $t$ . By the previous lemma, this monoid is $\mathcal{R}$ -trivial. Due to the local nature of the transitions of $A$ , if $a$ and $b$ are independent then $\Delta_{a}$ and $\Delta_{b}$ commute. As a result, we have a well defined morphism $h\colon TR(\tilde{\Sigma})\to M(A)$ which sends $t$ to $\Delta_{t}$ . Suppose that $L$ is accepted by $A$ with $s_{in}$ as the initial global state and $F$ as a subset of global accepting states of $A$ . Then $L$ is recognized by the trace morphism $h$ via the set $\{\Delta_{t}\in M(A)\mid\Delta_{t}(s_{in})\in F\}$ . Hence $L$ is $\mathcal{R}$ -trivial. $\hfill\blacktriangleleft$

5 Results on related fragments

In this section we briefly present other results which are of the same form as Theorem 2 but for trace languages which are $\mathcal{L}$ -trivial or recognized by monoids from the class DA. First we shall define the necessary terminology and then subsequently state the results.

$\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ is the fragment of temporal logic over traces which contains both the strict future ( $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ ) and the strict past ( $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ ) modality. We give below the syntax for $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ and only explain the semantics of the new modality $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ .

	$\displaystyle\Phi$	$\displaystyle::=\mathop{\mathsf{E}\vphantom{a}}\nolimits\varphi\mid\Phi_{1}% \lor\Phi_{2}\mid\lnot\Phi$
	$\displaystyle\varphi$	$\displaystyle::=a\mid\varphi_{1}\lor\varphi_{2}\mid\lnot\varphi\mid\mathop{% \mathsf{XF}\vphantom{a}}\nolimits\varphi\mid\mathop{\mathsf{YP}\vphantom{a}}\nolimits\varphi$

For a trace $t=(E,\leq,\lambda)$ and an event $e\in E$ , we have $t,e\models\mathop{\mathsf{XF}\vphantom{a}}\nolimits\varphi$ if there exists an event $f$ in $t$ with $e<f$ and $t,f\models\varphi$ . Observe that $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ is the past fragment of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ . We can similarly define $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ is as the future fragment of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ which has access to only $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ modality.

For a trace $t=(E,\leq,\lambda)$ , the reverse trace $t^{r}=(E,\leq^{\prime},\lambda)$ is defined to be the trace where, for $e,f\in E$ , $e\leq^{\prime}f$ iff $f\leq e$ . For a trace language $L\subseteq TR(\tilde{\Sigma})$ , the reverse language $L^{r}$ is defined as $L^{r}=\{t^{r}\mid t\in L\}$ .

For a monoid $M$ , $M^{r}$ denotes the opposite monoid with multiplication $\circ^{r}$ defined as $m\circ^{r}n:=n\circ m$ for all $m,n\in M^{r}$ . It is easy to see that $L$ is recognized by $M$ iff $L^{r}$ is recognized by $M^{r}$ . Further, it it easy to deduce that $M$ is $\mathcal{L}$ -trivial iff $M^{r}$ is $\mathcal{R}$ -trivial. It follows that $L$ is $\mathcal{L}$ -trivial iff $L^{r}$ is $\mathcal{R}$ -trivial.

It is also easy to verify that $L$ is $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ definable iff $L^{r}$ is $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ definable. Given a sentence $\Phi$ in $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ defining $L$ , we can obtain a $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ sentence $\Phi^{r}$ which defines $L^{r}$ by simply replacing all occurrences of $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ operators in $\Phi$ by $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ , and vice versa. In view of the above discussion, it follows from Theorem 2 that a trace language $L$ is $\mathcal{L}$ -trivial iff it is definable in $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ .

In order to obtain a translation of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ , or more generally, $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ event formulas and sentences into cascade products of asynchronous devices, as in Lemma 21 and Theorem 22 for $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ , we work with localized modalities $\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}$ and $\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}$ and use non-deterministic asynchronous automata/transducers.

We can define the localized logic $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i},\mathop{\mathsf{YP% }\vphantom{a}}\nolimits_{i}]}$ by using the process indexed modalities $\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}$ , $\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}$ and $\mathop{\mathsf{E}\vphantom{a}}\nolimits_{i}$ instead of $\mathop{\mathsf{XF}\vphantom{a}}\nolimits$ , $\mathop{\mathsf{YP}\vphantom{a}}\nolimits$ and $\mathop{\mathsf{E}\vphantom{a}}\nolimits$ as in Section 4.1. The semantics of $\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}$ modality is as follows: for a trace $t=(E,\leq,\lambda)$ and $e\in E$ , $t,e\models\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}\varphi$ iff $e$ is an $i$ -event and there exists an $i$ -event $f$ with $e<f$ such that $t,f\models\varphi$ . It can be shown that $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i},\mathop{\mathsf{YP% }\vphantom{a}}\nolimits_{i}]}$ has the same expressive power as $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ . Observe that $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ is a fragment of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i},\mathop{\mathsf{YP% }\vphantom{a}}\nolimits_{i}]}$ . One can similarly define the fragment $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}]}$ of $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i},\mathop{\mathsf{YP% }\vphantom{a}}\nolimits_{i}]}$ which has the same expressive power as $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ .

Now we turn our attention to local cascade product of non-deterministic asynchronous automata and transducers. For the purpose of this work, it suffices to work with deterministic and reverse deterministic versions and their cascade products.

We begin with the key example of the reverse deterministic asynchronous automata $U_{1}^{r}[i]$ . In $U^{r}_{1}[i]$ , the local state set of process $i$ has two states, that is, $S_{i}=\{1,2\}$ while all other processes have a singleton state set $S_{j}=\{1\}$ for $j\neq i$ . For a letter $a\not\in\Sigma_{i}$ , the processes participating in $a$ have a deterministic transition, namely, a self-loop.

Figure 2:

U_{1}^{r}[i]

automata: on the left is the local automaton for process

i

, on the right is the local single state automaton for every other process

j\neq i

.

If $a\in\Sigma_{i}=\Sigma_{i_{1}}\uplus\Sigma_{i_{2}}$ , we can identify a joint $a$ -state with the local state of process $i$ . With this identification, process $i$ has non-deterministic transitions as shown in Figure 2. For instance, assume $a\in\Sigma_{i_{2}}$ . Then there is no transition on $a$ at state $1$ . Further, at state $2$ , on $a$ , the next state can be either state $1$ or state $2$ . Note that these local transitions are obtained by simply reversing the local transitions in the deterministic $U_{1}[i]$ automata.

We always use the global state $1$ as the only final/accepting state. It is important to observe that, for a trace $t$ , $U^{r}_{1}[i]$ admits a unique accepting run $\rho_{t}$ (which ends in global state $1$ ). If $t$ has no $i$ -event with label in $\Sigma_{i_{2}}$ , then $\rho_{t}$ must begin in global state $1$ and stays there until the end. However, if $t$ has an $i$ -event with label in $\Sigma_{i_{2}}$ , then $\rho_{t}$ must begin in the global state $2$ and process $i$ component changes its local state from $2$ to $1$ on the last occurrence of an $i$ -event with label in $\Sigma_{i_{2}}$ . After this crucial event, process $i$ stays at local state $1$ as all subsequent “future” $i$ -events are labelled by letters in $\Sigma_{i_{1}}$ . This unambiguity property of $U_{1}^{r}[i]$ is crucial. While using $U_{1}^{r}[i]$ as a language acceptor, we allow a set of initial global states. Thanks to the unambiguity property, the language accepted with single initial global state $1$ is the complement of the language accepted with single initial global state $2$ .

Now we introduce the reverse deterministic asynchronous $\Gamma$ -transducers $\widehat{U_{1}^{r}[i]}$ . The underlying automaton of $\widehat{U_{1}^{r}[i]}$ is $U_{1}^{r}[i]$ and the output function provides a label from $\Gamma$ on each local transition of $U_{1}^{r}[i]$ . In $\widehat{U_{1}^{r}[i]}$ , we allow any initial global state but insist that $1$ is the only accepting state. We also associate with $\widehat{U_{1}^{r}[i]}$ a $\Gamma$ -labelling function $\widehat{U^{r}_{1}[i]}\colon TR(\tilde{\Sigma})\to TR(\widetilde{\Sigma\times% \Gamma})$ as follows: let $t=(E,\leq,\lambda)$ and $\rho_{t}$ be the unique accepting run of the underlying $U_{1}^{r}[i]$ on $t$ . We define $\widehat{U^{r}_{1}[i]}(t)$ to be the trace $t^{\prime}=(E,\leq,(\lambda,\mu))$ where, for $e\in E$ , $\mu(e)$ is the label from $\Gamma$ on the transition used to “read” $e$ on the unique run $\rho_{t}$ .

Let $\Gamma=\{\top,\bot\}$ . We now construct an instance of a $\Gamma$ -transducer $\widehat{U_{1}^{r}[i]}$ over $\Sigma\times\Gamma$ . This transducer, called $\widehat{U_{\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}}}$ below, implements the localized modality $\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}$ .

Figure 3:

\widehat{U_{\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}}}

transducer which implements

\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}

modality.

Consider a $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i},\mathop{\mathsf{YP% }\vphantom{a}}\nolimits_{i}]}$ formula $\varphi=\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}\varphi^{\prime}$ . We have the $\Gamma$ -relabelling functions $\theta^{\varphi^{\prime}}$ and $\theta^{\varphi}$ which keep track of truth values of $\varphi^{\prime}$ and $\varphi$ respectively. Let $t=(E,\leq,\lambda)$ be a trace over $\Sigma$ and $\theta^{\varphi^{\prime}}(t)=(E,\leq,(\lambda,\mu^{\prime}))$ and $\theta^{\varphi}(t)=(E,\leq,(\lambda,\mu))$ be traces over $\Sigma\times\Gamma$ . For any event $e$ of $t$ , $\mu^{\prime}(e)=\top$ iff $t,e\models\varphi^{\prime}$ and $\mu(e)=\top$ iff $t,e\models\varphi$ . Fix an event $e\in E$ . By semantics of $\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}$ , $\mu(e)=\top$ iff $e$ is an $i$ -event and there exists a strict future $i$ -event $f$ (that is, $e<f$ ) such that $\mu^{\prime}(f)=\top$ . For the $\Gamma$ -transducer $\widehat{U_{\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}}}$ over $\Sigma\times\Gamma$ , depicted in Figure 3, it is easy to verify that, for every trace $t$ over $\Sigma$ , $\widehat{U_{\mathop{\mathsf{XF}\vphantom{a}}\nolimits_{i}}}((\theta^{\varphi^{% \prime}}(t))=\theta^{\varphi}(t)$ .

In view of the above discussion, it is not surprising that the following theorem holds. We skip the technical details.

Theorem 25.

Let $L\subseteq TR(\tilde{\Sigma})$ . Then the following are equivalent.

1.

$L$ can be expressed by a sentence in $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ .
2.

$L$ can be accepted by a cascade product of $U_{1}[i]$ and $U^{r}_{1}[i]$ automata.

Even over words, the above result appears to be new. Further, we note that it has been shown in [17] (also see [11], [10]) that, over trace languages, $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits,\mathop{\mathsf{YP}% \vphantom{a}}\nolimits]}$ definability coincides with recognizability by monoids from the class DA.

The following theorem is a dual of our main theorem.

Theorem 26.

Let $L\subseteq TR(\tilde{\Sigma})$ . The following are equivalent.

1.

$L$ is a $\mathcal{L}$ -trivial trace language.
2.

$L$ can be expressed by a sentence in $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ .
3.

$L$ can be accepted by a cascade product of $U^{r}_{1}[i]$ automata.

Recall that a trace language is $\mathcal{J}$ -trivial iff it is $\mathcal{R}$ -trivial as well as $\mathcal{L}$ -trivial. This observation leads to the following result.

Theorem 27.

Let $L\subseteq TR(\tilde{\Sigma})$ . The following are equivalent.

1.

$L$ is a $\mathcal{J}$ -trivial trace language.
2.

$L$ can be expressed by a sentence in $\mathsf{LocTL[\mathop{\mathsf{XF}\vphantom{a}}\nolimits]}$ as well as a sentence in $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ .
3.

$L$ can be accepted by a cascade product of $U^{r}_{1}[i]$ automata as well as another cascade product of $U_{1}[i]$ automata.

References

[1] Bharat Adsul, Paul Gastin, Shantanu Kulkarni, and Pascal Weil. An expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3661814.3662110.
[2] Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Wreath/cascade products and related decomposition results for the concurrent setting of Mazurkiewicz traces. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 19:1–19:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPICS.CONCUR.2020.19.
[3] Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Asynchronous wreath product and cascade decompositions for concurrent behaviours. Log. Methods Comput. Sci., 18, 2022. doi:10.46298/LMCS-18(2:22)2022.
[4] Bharat Adsul and Milind A. Sohoni. Asynchronous automata-theoretic characterization of aperiodic trace languages. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 84–96. Springer, 2004. doi:10.1007/978-3-540-30538-5_8.
[5] Mikołaj Bojańczyk. Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic, 2020. arXiv:2008.11635.
[6] J.A. Brzozowski and Faith E. Fich. Languages of R-trivial monoids. Journal of Computer and System Sciences, 20(1):32–49, 1980. doi:10.1016/0022-0000(80)90003-3.
[7] Joëlle Cohen, Dominique Perrin, and Jean-Eric Pin. On the expressive power of temporal logic. Journal of Computer and System Sciences, 46(3):271–294, 1993. doi:10.1016/0022-0000(93)90005-H.
[8] Volker Diekert and Paul Gastin. Pure future local temporal logics are expressively complete for Mazurkiewicz traces. Information and Computation, 204(11):1597–1619, November 2006. doi:10.1016/J.IC.2006.07.002.
[9] Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci., 19(3):513–548, 2008. doi:10.1142/S0129054108005802.
[10] Volker Diekert, Martin Horsch, and Manfred Kufleitner. On first-order fragments for Mazurkiewicz traces. Fundamenta Informaticae, 80(1-3):1–29, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-02.
[11] Volker Diekert and Manfred Kufleitner. On first-order fragments for words and Mazurkiewicz traces: a survey. In Proceedings of the 11th international conference on Developments in language theory, pages 1–19, 2007.
[12] Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, 1995. doi:10.1142/2563.
[13] Werner Ebinger and Anca Muscholl. Logical definability on infinite traces. Theor. Comput. Sci., 154(1):67–84, 1996. doi:10.1016/0304-3975(95)00130-1.
[14] Kousha Etessami and Thomas Wilke. An until hierarchy and other applications of an Ehrenfeucht-Fraïsse game for temporal logic. Information and Computation, 160(1):88–108, 2000. doi:10.1006/inco.1999.2846.
[15] Giovanna Guaiana, Antonio Restivo, and Sergio Salemi. On aperiodic trace languages. In Christian Choffrut and Matthias Jantzen, editors, STACS 91, 8th Annual Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, February 14-16, 1991, Proceedings, volume 480 of Lecture Notes in Computer Science, pages 76–88. Springer, 1991. doi:10.1007/BFB0020789.
[16] Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. University of California, Los Angeles, CA, USA, 1968.
[17] Manfred Kufleitner. Polynomials, fragments of temporal logic and the variety $\mathrm{DA}$ over traces. Theoretical Computer Science, 376:89–100, 2007. Special issue DLT 2006. doi:10.1016/J.TCS.2007.01.014.
[18] Robert McNaughton and Seymour A Papert. Counter-Free Automata (MIT research monograph no. 65). The MIT Press, 1971.
[19] Madhavan Mukund and Milind A. Sohoni. Keeping track of the latest gossip in a distributed system. Distributed Comput., 10(3):137–148, 1997. doi:10.1007/s004460050031.
[20] M.P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.
[21] Howard Straubing. Finite automata, formal logic, and circuit complexity. Birkhaüser Verlag, Basel, Switzerland, 1994.
[22] Wolfgang Thomas. On logical definability of trace languages. In V. Diekert, editor, Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Kochel am See, Bavaria, FRG (1989), Report TUM-I9002, Technical University of Munich, pages 172–182, 1990.
[23] Wieslaw Zielonka. Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl., 21(2):99–135, 1987. doi:10.1051/ita/1987210200991.

[bib.bib1] [1] Bharat Adsul, Paul Gastin, Shantanu Kulkarni, and Pascal Weil. An expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3661814.3662110.

[bib.bib2] [2] Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Wreath/cascade products and related decomposition results for the concurrent setting of Mazurkiewicz traces. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 19:1–19:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPICS.CONCUR.2020.19.

[bib.bib3] [3] Bharat Adsul, Paul Gastin, Saptarshi Sarkar, and Pascal Weil. Asynchronous wreath product and cascade decompositions for concurrent behaviours. Log. Methods Comput. Sci., 18, 2022. doi:10.46298/LMCS-18(2:22)2022.

[bib.bib4] [4] Bharat Adsul and Milind A. Sohoni. Asynchronous automata-theoretic characterization of aperiodic trace languages. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 84–96. Springer, 2004. doi:10.1007/978-3-540-30538-5_8.

[bib.bib5] [5] Mikołaj Bojańczyk. Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic, 2020. arXiv:2008.11635.

[bib.bib6] [6] J.A. Brzozowski and Faith E. Fich. Languages of R-trivial monoids. Journal of Computer and System Sciences, 20(1):32–49, 1980. doi:10.1016/0022-0000(80)90003-3.

[bib.bib7] [7] Joëlle Cohen, Dominique Perrin, and Jean-Eric Pin. On the expressive power of temporal logic. Journal of Computer and System Sciences, 46(3):271–294, 1993. doi:10.1016/0022-0000(93)90005-H.

[bib.bib8] [8] Volker Diekert and Paul Gastin. Pure future local temporal logics are expressively complete for Mazurkiewicz traces. Information and Computation, 204(11):1597–1619, November 2006. doi:10.1016/J.IC.2006.07.002.

[bib.bib9] [9] Volker Diekert, Paul Gastin, and Manfred Kufleitner. A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci., 19(3):513–548, 2008. doi:10.1142/S0129054108005802.

[bib.bib10] [10] Volker Diekert, Martin Horsch, and Manfred Kufleitner. On first-order fragments for Mazurkiewicz traces. Fundamenta Informaticae, 80(1-3):1–29, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-02.

[bib.bib11] [11] Volker Diekert and Manfred Kufleitner. On first-order fragments for words and Mazurkiewicz traces: a survey. In Proceedings of the 11th international conference on Developments in language theory, pages 1–19, 2007.

[bib.bib12] [12] Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, 1995. doi:10.1142/2563.

[bib.bib13] [13] Werner Ebinger and Anca Muscholl. Logical definability on infinite traces. Theor. Comput. Sci., 154(1):67–84, 1996. doi:10.1016/0304-3975(95)00130-1.

[bib.bib14] [14] Kousha Etessami and Thomas Wilke. An until hierarchy and other applications of an Ehrenfeucht-Fraïsse game for temporal logic. Information and Computation, 160(1):88–108, 2000. doi:10.1006/inco.1999.2846.

[bib.bib15] [15] Giovanna Guaiana, Antonio Restivo, and Sergio Salemi. On aperiodic trace languages. In Christian Choffrut and Matthias Jantzen, editors, STACS 91, 8th Annual Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, February 14-16, 1991, Proceedings, volume 480 of Lecture Notes in Computer Science, pages 76–88. Springer, 1991. doi:10.1007/BFB0020789.

[bib.bib16] [16] Johan Anthony Willem Kamp. Tense Logic and the Theory of Linear Order. University of California, Los Angeles, CA, USA, 1968.

[bib.bib17] [17] Manfred Kufleitner. Polynomials, fragments of temporal logic and the variety $\mathrm{DA}$ over traces. Theoretical Computer Science, 376:89–100, 2007. Special issue DLT 2006. doi:10.1016/J.TCS.2007.01.014.

[bib.bib18] [18] Robert McNaughton and Seymour A Papert. Counter-Free Automata (MIT research monograph no. 65). The MIT Press, 1971.

[bib.bib19] [19] Madhavan Mukund and Milind A. Sohoni. Keeping track of the latest gossip in a distributed system. Distributed Comput., 10(3):137–148, 1997. doi:10.1007/s004460050031.

[bib.bib20] [20] M.P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.

[bib.bib21] [21] Howard Straubing. Finite automata, formal logic, and circuit complexity. Birkhaüser Verlag, Basel, Switzerland, 1994.

[bib.bib22] [22] Wolfgang Thomas. On logical definability of trace languages. In V. Diekert, editor, Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Kochel am See, Bavaria, FRG (1989), Report TUM-I9002, Technical University of Munich, pages 172–182, 1990.

[bib.bib23] [23] Wieslaw Zielonka. Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl., 21(2):99–135, 1987. doi:10.1051/ita/1987210200991.

Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Preliminaries

2.1 Trace basics

2.2 Recognizable trace languages

Example 1.

3 Algebra to temporal logic

Theorem 2.

Proof.

3.1 𝗟𝗼𝗰𝗧𝗟⁢[𝗬𝗣] syntax and semantics

Example 3.

3.2 Critical structures for a morphism into a 𝓡-trivial monoid

Lemma 4.

Proof.

Lemma 5.

Proof.

Example 6.

Lemma 7.

Proof.

Example 8.

Lemma 9.

Proof.

Corollary 10.

Lemma 11.

Proof.

3.3 Proof of Theorem 2 [𝟏→𝟐]

Lemma 12.

Proof.

Lemma 13.

Proof.

Theorem 14.

Proof.

4 Logic to cascade products to algebra

4.1 𝗟𝗼𝗰𝗧𝗟⁢[𝗬𝗣𝗶] and its equivalence with 𝗟𝗼𝗰𝗧𝗟⁢[𝗬𝗣]

Lemma 15.

Proof.

▶ Remark 16.

4.2 Asynchronous devices and cascade product

Example 17.

Example 18.

Definition 19.

Lemma 20.

4.3 Proof of Theorem 2 [𝟐→𝟑]

Lemma 21.

Proof.

Theorem 22.

Proof.

4.4 Proof of Theorem 2 [𝟑→𝟏]

Lemma 23.

Proof.

Theorem 24.

Proof.

5 Results on related fragments

Theorem 25.

Theorem 26.

Theorem 27.

References

3.1 $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$ syntax and semantics

3.2 Critical structures for a morphism into a $\mathcal{R}$ -trivial monoid

3.3 Proof of Theorem 2 [ $1\to 2$ ]

4.1 $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits_{i}]}$ and its equivalence with $\mathsf{LocTL[\mathop{\mathsf{YP}\vphantom{a}}\nolimits]}$

$\blacktriangleright$ Remark 16.

4.3 Proof of Theorem 2 [ $2\to 3$ ]

4.4 Proof of Theorem 2 [ $3\to 1$ ]