Omega Automata PlugIn

This plug-in provides data structures and functions to represent automata that process infinite-length words. For a general overview on the topic see [W1]. For the purpose of libFAUDES, we restrict the scope to support for synthises of supervisiors for non-termiating processes.

Further details are organized as follows:



Copyright (C) 2010, 2025 Thomas Moor.

Acceptance Conditions

Consider a genarator G and ignore that marking for now; we use the notation

G  =  (Q, Sigma, delta, Qo,  . )

with alphabet Sigma, state set Q, transition relation delta ⊆ Q x Sigma x Q, and initial states Qo. Assuming that G is free of deadlocks it can likewise model a non-terminating process. Denoting L(G) the generated star-language, we associate with G the generated omega-language

B(G)  :=  {v ∈ Sigma^w | all prefixes s < v are in L(G) }.

The crucial aspect from the infinite-length words perspective is the acceptance condition, a technical construct that after the elapse of all time decides whether or not a processed word w ∈ B(G) shall be considered an element of the accepted omega language. We recall two well established acceptance conditions.

Buechi Automata

A Buechi automaton technically matches the plain finite automaton; i.e., has the form G = (Q, Sigma, delta, Qo, Qm) with the marked states Qm. With an infinite-length run pi on G we associate

  • w[pi] the corrosponding infinite-length word over Sigma, and

  • inf[pi] the set of states that have been visited infinitely often.

An infinite-length word v is accepted by the Buechi automaton G if there exists a correspondimg run pi that visits at least one marked state infinitely often. The accepted omega-language associated with G is hence defined

Bm(G)  :=  {v ∈ Sigma^w | there ex. a run pi of G with v = w[pi] and inf[pi] ∩ Qm ≠ 0}

For deterministic generators, Bm(G) can be expressed as the limit of Lm(G):

Bm(G)  =  B(Lm(G))  :=  {w ∈ Sigma^v | infinitely many prefixes s < v are in Lm(G) } .

In particular, for deterministic generators G1 and G2 with Lm(G1) = Lm(G2) we have Bm(G1) = Bm(G2).

Rabin Automata

A Rabin automaton is a tuple G = (Q, Sigma, delta, Qo, A), where the first entries are as for common automata and A is a set of pairs if state sets to encode a Rabin acceptance condition. Technically we have

A := { (Rp, Ip) | p ∈ P } with Rp, Ip ⊆ Q for all p ∈ P .

For an individual pair (Rp, Ip), p ∈ P, the set Rp shall be persistently recurrent and the set Ip shall be an eventually invariant. An infinite-length run pi on G is accepted w.r.t. the pair (Rp, Ip) if it pi eventually stays within Ip and visits Rp infinitely often, i.e.,

inf[pi] ⊆ Ip and inf[pi]∩Rp ≠ 0 .

The run is accepted by the Rabin automaton if it is accepted by at least one pair (so called existential Rabin acceptace condition). Thus we have the associated omega-language

Rm(G)  :=  {v ∈ Sigma^w | there ex. a run pi of G and p ∈ P s.t. v = w[pi], inf[pi] ⊆ Ip and inf[pi]∩Rp ≠ 0 }

Literature

[W1] W. Thomas: Automata on infinite objects, Handbook of Theoretical Computer, 1990.

[W2] P.J. Ramadge: Some tractable supervisory control problems for discrete-event systems modeled by Buchi automata, IEEE Transactions on Automatic Control, vol 34, no 1, pp. 10-19, 1989.

[W3] R. Kumar, V. Garg, S.I. Marcus: On supervisory control of sequential behaviors, IEEE Transactions on Automatic Control, vol 37, no 12, pp. 1978-1985, 1992.

[W4] J.G. Thistle, W.M. Wonham: Supervision of Infinite Behavior of Discrete-Event Systems, SIAM Journal on Control and Optimization, vol 32, no, 4, pp. 1098 - 1113, 1994.

libFAUDES 2.33h --- 2025.06.17 --- with "synthesis-omegaaut-observer-diagnosis-iosystem-hiosys-multitasking-coordinationcontrol-timed-iodevice-priorities-simulator-luabindings"

>>