Unifying Asynchronous Logics for Hyperproperties
Alberto Bombardelli Laura Bozzelli César Sánchez Stefano Tonetta

The Directed Landscape is a Black Noise
    [
    April 29, 2024
=======================================


We introduce and investigate a powerful hyper logical framework in the linear-time setting, we call
generalized  with stuttering and contexts ( for short). 
  unifies  known asynchronous extensions of  and  the well-known extension  of  with  knowledge modalities under both the synchronous and asynchronous perfect recall semantics.
As a main contribution, we individuate a meaningful fragment of , we call  simple , with a decidable model-checking problem,
which is more expressive than  and known fragments of asynchronous extensions of  with a decidable model-checking problem.
Simple  subsumes  under the synchronous semantics and the one-agent fragment of  under the asynchronous semantics, and to the best
of our knowledge, it represents the unique hyper logic with a decidable model-checking problem which can express powerful non-regular trace properties when interpreted on singleton sets of traces. We justify the relevance of simple  by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt ).
  
 
  
 
  
 
 
  



  

§ INTRODUCTION


Temporal logics <cit.> play a fundamental role in the  formal
verification  of the dynamic behaviour of complex reactive systems.
Classic regular temporal logics such as , , and
 <cit.> are suited for the specification of
 trace properties which describe  the ordering of events along individual execution
traces of a system. In the last decade, a novel specification paradigm has been introduced
that generalizes traditional regular trace properties by properties of
sets of traces, the so called
hyperproperties <cit.>.
Hyperproperties relate distinct traces and are useful to formalize a wide range of properties
of prime interest which go, in general,
 beyond regular properties and cannot be expressed in standard regular temporal logics.
 A relevant example  concerns information-flow security policies like
noninterference <cit.> and observational
determinism <cit.>  which compare observations made by an
external low-security agent along traces resulting from different
values of not directly observable inputs. Other examples include bounded termination of programs,
diagnosability of critical systems (which amounts to checking whether the available sensors information is sufficient
to infer the presence of faults on the hidden behaviour of the system) <cit.>, and epistemic properties describing the
 knowledge  of agents in distributed systems <cit.>.

 In the context of model checking of finite-state reactive systems, many temporal logics for hyperproperties have been proposed <cit.>
for which model checking is decidable, including
 <cit.>,  <cit.>,
 <cit.>, and  <cit.>
which extend , ,  <cit.>, and
 <cit.>, respectively, by explicit first-order
quantification over traces and trace variables to refer to multiple
traces at the same time. The semantics of all these logics is synchronous
and the temporal modalities are evaluated by a
lockstepwise traversal of all the traces assigned to the quantified
trace variables. Other  approaches for the formalization of synchronous hyper logics are either based on hyper variants
of monadic second-order logic over traces or trees <cit.>, or the
adoption of a team semantics for standard temporal logics, in particular,  <cit.>.
For the first approach in the linear-time setting,
we recall the logic  <cit.> (and its first-order fragment  <cit.>)
which syntactically  extends monadic second-order logic of one successor  with the equal-level predicate
, which relate the same time point on different traces. More recently, an extension of  with second-order quantification over traces
has been introduced <cit.> which allows to express common knowledge in multi-agent distributed systems. Like , model checking of this extension
  of  is highly undecidable <cit.>. 

Hyper logics supporting asynchronicity features have been introduced recently <cit.>.
These logics allow to relate traces at distinct time points which can be arbitrarily far
from each other. Asynchronicity is ubiquitous in many real-world systems, for example, in multithreaded environments in which threads are not scheduled lokstepwise,
and traces associated with distinct threads progress with different speed.
Asynchronous hyperproperties  are also useful in information-flow security and diagnosability settings where an
observer cannot distinguish
consecutive time points along an execution having the same
observation. This requires asynchronously matching sequences of observations along
distinct execution traces.
 The first systematic study of asynchronous hyperproperties was done by Gutsfeld et al. <cit.>, who introduced
 the  temporal fixpoint calculus  and its automata-theoretic counterpart for expressing such class of properties in the linear-time
 setting. More recently, three temporal logics <cit.> which syntactically extend  have been introduced
for expressing  asynchronous hyperproperties:  Asynchronous 
() <cit.> and  Stuttering  () <cit.>, both
useful for asynchronous security analysis, and Context  (), useful for expressing hyper-bounded-time response
requirements. The logic  , which is expressively incomparable with both  and  <cit.>, models asynchronicity   by means of an additional quantification layer over the so called trajectories which control  the relative speed at which traces progress by choosing
 at each instant which traces move and which traces stutter. On the other hand, the logic 
 exploits relativized versions of
the temporal modalities with respect to finite sets Γ of 
formulas: these modalities are evaluated by a lockstepwise traversal of the sub-traces of the
given traces which are obtained by removing “redundant” positions
with respect to the pointwise evaluation of the  formulas in
Γ. Finally, the logic  (which is not expressively subsumed  by both  and  <cit.>) extends  by unary modalities C parameterized by
a non-empty subset C of trace variables—called the
context—which restrict the evaluation of the temporal
modalities to the traces associated with the variables in C. It is known that these three syntactical extensions of  are less expressive than

 <cit.> and like , model checking  the respective quantifier  alternation-free
fragments are already undecidable <cit.>. The works <cit.> identify practical fragments
of the logics  and  with a decidable model checking problem. In particular, we recall the so called  simple fragment of  <cit.> which is more expressive than  <cit.>, and can specify interesting security policies in the asynchronous setting. Formalization of asynchronous hyperpropries in the team semantics setting following an approach similar to the trajectory construct of  has been investigated in <cit.>. It is worth noting that unlike other hyper logics (including logics with team semantics) which only capture regular trace properties when interpreted on singleton sets of traces, the logics , , and  can express non-regular trace properties <cit.>. 


Our contribution. Specifications in  and in the known asynchronous extensions of , whose most expressive representative is 
  <cit.>, consist  of a prefix of trace quantifiers followed by a quantifier-free formula which expresses temporal requirements on a fixed number of traces. Thus, these hyper logics lack mechanisms to relate directly an unbounded number of traces, which are required for example to express bounded termination or diagnosability properties <cit.>. This ability is partially supported by temporal logics with team semantics <cit.> and extensions of temporal logics
with the knowledge modalities of epistemic logic <cit.>, which
relate computations whose histories are observationally equivalent for a
  given agent. In this paper, we introduce and investigate an hyper logical framework in the linear-time setting which unifies two known asynchronous extensions of  and  the well-known extension  <cit.> of  with  knowledge modalities under both the
  synchronous and asynchronous perfect recall semantics (where an agent remembers the
  whole sequence of its observations). The novel logic, we call generalized  with stuttering and contexts ( for short),
merges  and  and adds two
new natural modeling facilities: past temporal modalities for asynchronous hyperproperties and general trace quantification where trace quantifiers can occur in
the scope of temporal modalities. Past temporal modalities used in combination with context modalities provide a powerful mechanism to compare histories of computations at distinct time points. Moreover, unrestricted trace quantification allows to relate an unbounded number of traces.

As a main contribution, we individuate a meaningful fragment of  with a decidable model-checking problem, we call  simple ,
which is obtained from  by carefully imposing restrictions on the use of the stuttering and context modalities. This fragment allows quantification over arbitrary pointed traces (i.e., traces plus time points) in the style of  <cit.>), it is more expressive than the simple fragment of  <cit.>, and it is expressively incomparable with full  and . Moreover, this fragment subsumes both  under the synchronous semantics and the one-agent fragment of  under the asynchronous semantics. In fact, simple  can be seen as the
maximal fragment of  with a decidable model checking problem which strictly subsumes   and the simple fragment of , is closed under Boolean connectives, and allows an unrestricted nesting of temporal modalities. We justify the relevance of simple  by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt  <cit.>). To the best of our knowledge, simple   represents the unique hyper logic with a decidable model-checking problem which  can express powerful non-regular trace properties when interpreted on singleton sets of traces. 






  

§ BACKGROUND


We denote by  the set of natural numbers.

Given i,j∈, we write [i,j] for the set of natural numbers
h such that i≤ h≤ j, we use [i,j) for the set
[i,j]∖{j}, we use (i,j] for the set
[i,j]∖{i}, and [i,∞] for the set of natural numbers
h such that h≥ i.

Given a word w over some alphabet Σ, |w| is the length of
w (|w|=∞ if w is infinite).

For each 0≤ i<|w|, w(i) is the (i+1)^th symbol of w,
w^i is the suffix of w from position i, that is, the word
w(i)w(i+1)…, and w[0,i] is the prefix of w that ends at
position i.

We fix a finite set  of atomic propositions.

A trace is an infinite word over 2^, while a finite trace is a
nonempty finite word over 2^.

A pointed trace is a pair (,i) consisting of a trace
 and a position (timestamp) i∈ along
.



Standard  with past ( for
short) <cit.>.




 Formulas φ of  over the given finite set  of atomic propositions
 are defined by the following grammar: 
 

    φ ::= ⊤|  p  |φ|φ∨φ|φ|φ|φφ|φφ


where p∈,  and  are the next and
until temporal modalities respectively, and 
(previous or yesterday) and  (since) are
their past counterparts.

 is the fragment of  that does not contain the past
temporal modalities  and .

We also use the following abbreviations:
φ:=⊤φ (eventually),
φ:=⊤φ (past eventually or
once), and their duals
φ:=φ (always) and
φ:=φ (past always or
historically).

The semantics of  is defined over pointed traces (,i).

The satisfaction relation (,i)φ, that defines
whether formula φ holds at position i along , is
inductively defined as follows (we omit the semantics for the Boolean
connectives which is standard): 
 

    [                                                       (, i)   p                                                       ⇔  p ∈(i);                                                           (,i)φ                                                       ⇔ (,i+1)φ;                                                           (,i)φ                                             ⇔ i>0  and  (,i-1)φ;                                                    (, i) φ_1φ_2  ⇔for some j≥ i: (, j)
      φ_2
       and   (, k) φ_1  for all i≤ k<j;                                                    (, i) φ_1φ_2 ⇔for some j≤ i: (, j)
      φ_2
       and   (, k) φ_1  for all j< k≤ i;                                                                 ]

 
A trace  is a model of φ, written
φ, whenever (,0)φ.

 



Kripke structures.

We define the dynamic behaviour of a reactive system by 
Kripke structures =,_0,,
over a finite set  of atomic propositions, where 
 is a set of states, _0⊆ is the set of initial
states, ⊆× is a transition
relation   which is total in the first argument (i.e., for each
∈ there is a '∈ with
(,')∈), and :→ 2^ is a labeling map 
assigning to each state  the set of
propositions holding at .

The Kripke structure  is finite if  is finite.

A path  of  is an infinite word
= _0,_1,… over  such that _0∈_0  and for all
i≥ 0, (_i,_i+1)∈.

The path = _0,_1,… induces the trace
(_0)(_1)….

A trace of   is a trace induced by some path of .



We also consider fair finite Kripke structures
(,), that is, finite Kripke structures
 equipped with a subset  of -states.

A path  of  is -fair if  visits
infinitely many times some state in .

We denote by (,) the set of traces of
 associated with the -fair paths of
. 

 

  

§ UNIFYING FRAMEWORK FOR ASYNCHRONOUS EXTENSIONS OF
HYPERLTL



 In this section, we introduce a novel logical framework for specifying asynchronous linear-time hyperproperties which
 unifies two known asynchronous extensions of  <cit.>, namely
 Stuttering  ( for short) <cit.> and
Context  ( for short) <cit.>.














The proposed hyper logic, we call generalized  with stuttering and contexts ( for short),
merges  and  and adds two
new features: past temporal modalities for asynchronous hyperproperties and general trace quantification where trace quantifiers can occur in
the scope of temporal modalities. Since model checking of the logics  and  is already undecidable <cit.>, we also
consider a meaningful fragment of  which is strictly more expressive than the known simple fragment of  <cit.>. Our fragment is
able to express relevant classes of hyperproperties and, as we show in Section <ref>,  its (fair) model checking problem  is decidable.









 §.§ PLTL-Relativized Stuttering



Classically, a trace is stutter-free if there are no consecutive
positions having the same propositional valuation unless the valuation
is repeated ad-infinitum.

We can associate to each trace a unique stutter-free trace by removing
“redundant” positions.

The logic  <cit.>  generalizes these notions with respect to the
pointwise evaluation of a finite set of  formulas. Here, we
consider  with past ().

 <cit.>
  Let Γ be a finite set of  formulas and  a
  trace.
  
  The Γ-stutter factorization of  is the unique
  increasing sequence of positions {i_k}_k∈[0,m_∞] for
  some m_∞∈∪{∞} such that the following holds
  for all j <m_∞:
  
  
  
  * i_0=0 and i_j<i_j+1;
  
  * for each θ∈Γ, the truth value of θ along
    the segment [i_j,i_j+1) does not change, for all
    h,k∈ [i_j,i_j+1), (,h)θ iff
    (,k)θ, and the same holds for the infinite segment
    [m_∞, ∞] in case m_∞≠∞;
  
  * the truth value of some formula in Γ changes along
    adjacent segments, for some θ∈Γ (depending on
    j), (,i_j)θ iff (,i_j+1)θ.




Thus, the Γ-stutter factorization
{i_k}_k∈[0,m_∞] of  partitions the trace in
adjacent non-empty segments such that the valuation of formulas in
Γ does not change within a segment, and changes in moving from
a segment to the adjacent ones.

This factorization induces in a natural way a trace obtained by
selecting the first positions of the finite segments and all the
positions of the unique infinite segment, if any. These positions
form an infinite increasing sequence {ℓ_k}_k∈ called (Γ,ω)-stutter factorization of ,
where:


    ℓ_0,ℓ_1, …
        i_0,i_1,…   if  m_∞=∞
    
        i_0,  i_1, …,  i_m_∞, i_m_∞+1,…   otherwise


The Γ-stutter trace of  <cit.>, denoted by
_Γ(), is defined as follows: _Γ()(ℓ_0)(ℓ_1)….
 Note that for Γ=∅, _Γ()=. A trace  is Γ-stutter free if it coincides with its Γ-stutter trace, _Γ()=.

As an example, assume that ={p,q,r} and let
Γ= {p q}.

Given h,k≥ 1, let _h,k be the trace
_h,k = p^h q^k r^ω.

These traces have the same Γ-stutter trace 
given by p r^ω.








The semantics of the Γ-relativized temporal modalities
in  is based on the notion of Γ-successor _Γ(,i) of a pointed trace (,i) <cit.>:
_Γ(,i) is the  trace (,ℓ)
where ℓ is the smallest position ℓ_j in the
(Γ,ω)-stutter factorization {ℓ_k}_k∈ of  which is greater than i.
Note that for Γ=∅,  _∅(,i)=(,i+1), which captures the standard local successor of a position along a trace.

In this paper we extend  with past temporal modalities, so that  we introduce the past counterpart
of the successor function. The Γ-predecessor _Γ(,i) of a pointed trace
(,i) is undefined if i=0 (written _Γ(,i)=); otherwise,
_Γ(,i) is the trace (,ℓ)
where ℓ is the greatest position ℓ_j in the
(Γ,ω)-stutter factorization {ℓ_k}_k∈ of  which is smaller than i (since ℓ_0=0 such an ℓ_j exists).
Note that for Γ=∅, _∅(,i) captures the standard local predecessor of a position along a trace.












 §.§ Generalized HyperLTL with stuttering and contexts


We introduce now the novel logic .

For the given finite set  of atomic propositions and a finite set  of trace variables, the set of formulas φ of  over
 and  is defined by the following syntax:


    φ :=⊤|p|φ|φ∨φ|∃. φ|φ|_Γφ|_Γφ|φ_Γφ|φ_Γφ

 
where p∈, ∈,
∃ is the
hyper existential trace quantifier for variable ,
  is the context modality
with ∅≠⊆, Γ is a finite set of  formulas,
and _Γ, _Γ,  _Γ and _Γ are the
stutter-relativized versions of the  temporal modalities.
Intuitively, the context modality 
 restricts the evaluation of the temporal
modalities to the traces associated with the variables in , while
the temporal modalities _Γ, _Γ,  _Γ and _Γ
are evaluated by a
lockstepwise traversal of the Γ-stutter traces associated to the traces assigned to the  variables in the current context .
 Note that p is the -relativized version of proposition p which intuitively asserts that p holds at the pointed trace assigned to variable x.
We also exploit the hyper universal  quantifier ∀ as abbreviation:
∀. φ::= ∃. φ. For a  variable
, we write  instead of {}.
Moreover, we write , ,   and  instead of
_∅, _∅,  _∅ and _∅, respectively.
Furthermore, for a  formula ψ and a   variable ,
   we write ψ for the formula obtained from ψ by replacing each  proposition p with its -version
p.
 A sentence is a formula
where each relativized proposition p occurs in the scope of trace quantifier
∃ or ∀, and each temporal modality occurs in the scope of a trace quantifier.


 The known logics  , ,  , and simple . A formula φ of   is in prenex form
  if it is of the form _1_1. …_n_n. ψ where ψ is quantifier-free and  _i∈{∃,∀}
  for all i∈ [1,n]. The logics  <cit.>,   <cit.>, and  <cit.>  correspond to  syntactical fragments of
   where the formulas are in prenex form and past temporal modalities are not used. Moreover, in , the context modalities are not allowed, while in , the subscript Γ of every temporal modality must be the empty set. In standard  <cit.>, both the context modalities and the temporal modalities where the subscript Γ is not empty are disallowed. Finally, we recall the simple fragment of  <cit.>, which
  is more expressive than  and is parameterized by a finite set Γ of  formulas. The  quantifier-free formulas  of simple  for the parameter Γ are defined
as  Boolean combinations of formulas of  the form ψ, where ψ is an  formula, and formulas ψ_Γ  defined by the following grammar:


    ψ_Γ :=  ⊤|p|ψ_Γ|ψ_Γ∨ψ_Γ|_Γψ_Γ|ψ_Γ_Γψ_Γ


Trace assignments, successors and predecessors.  In order to define the semantics of , we need additional definitions.
Given a set of traces , a (pointed) trace assignment over 
is a  partial mapping : →× assigning to each trace variable
—where  is defined—a pointed trace (,i) such that ∈.
We use () to refer to the trace variables for which  is defined.
Given a  trace variable ∈ and a pointed trace (,i) with ∈,
we denote by [↦ (,i)] the trace assignment that is identical
to  besides for , which is mapped to (, i).

Let   be a trace assignment over some set of traces ,  Γ be a finite set of  formulas,
and  be a context. The (Γ,)-successor of
, denoted by _(Γ,)(),  is the trace assignment over   having domain
 (), and defined as follows for each ∈():


    _(Γ,)()() :=
      _Γ(())    if ∈
    ()    otherwise


Moreover, we define the (Γ,)-predecessor _(Γ,)() of
  as follows:
 _(Γ,)() is undefined, written _(Γ,)()=, if
 there is ∈() such that _Γ(())=. Otherwise,
 _(Γ,)()  is the trace assignment over   having domain
 (), and defined as follows for each ∈():


    _(Γ,)()() :=
      _Γ(())    if ∈
    ()    otherwise


 Finally, for each i≥ 0, we define the i^th application ^i_(Γ,) of _(Γ,) and
 the i^th application ^ i_(Γ,) of _(Γ,) as follows:
 
  
    ^i_(Γ,)() :=
         if  i = 0
    _(Γ,)(^i-1_(Γ,)())     otherwise



    ^ i_(Γ,)() :=
         if  i = 0
       if  i > 0  and ^ i-1_(Γ,)=
    _(Γ,)(^ i-1_(Γ,)())     otherwise




Semantics of . Given a formula φ, a set of traces ,
a trace assignment  over  such that () contains all the trace variables occurring free in φ, and a context ⊆,
the satisfaction relation (, ) _φ, meaning that the assignment  over  satisfies
φ under the context ,
  is inductively defined as follows (we omit the semantics of the Boolean connectives which is standard): 


    [                                                            (, ) _p                                         ⇔() = (,i)  and 
        p∈(i);                                                         (, ) _∃. φ                                ⇔ for some ∈, 
        ([↦ (, 0)], ) _φ;                                                         (, ) _∀. φ                                 ⇔ for all ∈, 
        ([↦ (, 0)], ) _φ;                                                           (, ) _'φ                                                       ⇔   (, ') _φ;                                                          (, ) __Γψ                                                    ⇔  (_(Γ,)(),) ψ;                                                          (, ) __Γψ                                     ⇔_(Γ,)() ≠ and  (_(Γ,)(), ) _φ;                                                    (, ) _ψ_1 _Γψ_2                  ⇔there is  i≥ 0  such that (^i_(Γ,)(),) _ψ_2  and;                                                                                             ⇔ for all  0 ≤ j < i,  (^j_(Γ,)(), ) _ψ_1;                                                    (, ) _ψ_1 _Γψ_2 ⇔there is  i≥ 0  such that  ^ i_(Γ,)() ≠,
          (^ i_(Γ,)(),) _ψ_2;                                                                                         ⇔and for all  0 ≤ j < i,  (^ j_(Γ,)(), ) _ψ_1 ]

 
For a sentence φ and a set of traces ,  is a model of φ, written φ if
(_∅, ) _φ where _∅ is the trace assignment with empty domain.



Fair-model checking decision problem.

Given a fragment  of , 

the fair model checking problem for  consists on deciding,
given a fair finite Kripke structure (,) and a sentence
φ of , whether (,)φ.

The previous problem is simply called model checking problem
whenever  coincides with the set of -states.





 §.§ The simple fragment of 


We introduce now a fragment of , we call simple , which syntactically subsumes the simple fragment of  <cit.>.


In order to define the syntax of simple , we first consider some shorthands. The pointed existential quantifier ∃^ is defined
 as follows: ∃^. φ ::= ∃. φ. Moreover, the pointed universal
   quantifier ∀^ is defined as: ∀^. φ::= ∃^. φ.
   Thus the pointed quantifiers quantify on arbitrary pointed traces over the given set of traces and set the global context for the given operand.
Simple   is parameterized by a finite set Γ of  formulas. The set of formulas φ_Γ in the Γ-fragment is defined
as follows: 
 

    φ_Γ :=   ⊤|ψ|φ_Γ|φ_Γ∨φ_Γ|∃. φ_Γ|∃^. φ_Γ|_Γφ_Γ|_Γφ_Γ|φ_Γφ_Γ|φ_Γφ_Γ

 
where ψ is a  formula. Note that for an atomic proposition p,
xp corresponds to p. Moreover, ∃. φ corresponds
to ∃^. (φ∧⊤).
The Γ-fragment of simple  is denoted by Γ.
We say that a formula φ of simple  is singleton-free if for each subformula  xψ of φ, ψ is an atomic proposition.

In Section <ref>, we will show that (fair) model checking of simple  is decidable. In fact, simple  can be seen as the
maximal fragment of  with a decidable model checking problem which subsumes the simple fragment of , is closed under Boolean connectives, and allows an unrestricted nesting of temporal modalities. Maximality is justified by the following known undecidability results.

  
  * Model checking of  is already undecidable <cit.> for sentences whose relativized temporal  modalities exploit two distinct sets of  formulas, and, in particular, for two-variable quantifier alternation-free  sentences of the form ∃_1. ∃_2. (φ∧_Γψ), where ψ is a propositional formula, Γ is a nonempty set of propositions, and φ is a quantifier-free formula which use only the temporal modalities _∅ and _∅.
  
  * Model checking of  is undecidable <cit.> even for the fragment  consisting of two-variable quantifier alternation-free sentences of the form ∃_1.∃_2. ψ_0∧_2{_1,_2}ψ, where ψ_0 and ψ are quantifier-free  formulas (note that ψ_0 is evaluated in the global context {_1,_2}).



The second undecidability result suggests to consider the  extension of simple  where singleton-context subformulas of the form
ψ  are replaced with   quantifier-free  formulas  with multiple variables
of the form ξ, where ξ  only uses singleton contexts  and temporal modalities with subscript ∅. However, we can show that  the resulting logic is not more
expressive than simple : a sentence in the considered extension can be translated into an equivalent simple  sentence
though with a non-elementary blowup (for details, see Appendix <ref>).




 §.§ Examples of Specifications in Simple
  



We consider some relevant properties which can be expressed in simple
. 

Simple  subsumes the simple fragment of , and this
fragment (as shown in <cit.>) can express relevant
information-flow security properties for asynchronous frameworks such
as distributed systems or cryptographic protocols.

An example is the asynchronous variant of the noninterference
property, as defined by Goguen and Meseguer <cit.>,
which asserts that the observations of low users (users accessing
only to public information) do not change when all inputs of high
users (users accessing secret information) are removed.

Another example is observational determinism, which states that
traces which have the same initial low inputs are indistinguishable to
a low user.

In an asynchronous setting, a user cannot infer that a transition
occurred if consecutive observations remain unchanged.

Thus, for instance, observational determinism with equivalence of
traces up to stuttering (as formulated in <cit.>) can be
captured by the following simple  sentence, where LI (resp.,
LO) is the set of propositions describing inputs (resp., output) of
low users. 


    ∀. ∀. ⋀_p∈ LI  (p↔p) →_LO⋀_p∈ LO (p↔p)

 
Moreover, simple  allows to specify complex
combinations of asynchronous and synchronous constraints.

As an example, we consider the property <cit.> that for
an  sentence
Q_1 _1. … Q_n_n. ψ(_1,…,_n), the quantifier-free formula
ψ(_1,…,_n) holds along the traces bound by
variables _1…,_n after an initialization
phase.

Note that this phase can take a different and unbounded number of
steps on each trace.

Let  be a proposition characterizing the initialization phase, and 
let
()
(∧(⊤∨))

be a simple  formula asserting that for the pointed trace (,i) assigned to variable ,  
 i is the first position
of  following the initialization phase.

Then, the previous requirement can be expressed in simple  as
follows, where ∃^∈. φ is a shorthand
for ∃^. (()∧φ) and
∀^∈. φ is a shorthand for
∀^. ( () →φ):
 

    Q_1^_1∈. … Q_n^_n∈. ψ(_1,…,_n)


As another meaningful example, we consider global promptness
(in the style of Prompt  <cit.>), where one need
to check for a uniform bound k on the response time in all the
traces of the system, “there is k such that for every
  trace, each request q is followed by a response p within k
  steps”. Global promptness is expressible in simple 
as: 
  

    ∃^. (q ∧ ∀^.   (q→  (p  p)) )


Diagnosability. We now show that simple  is
able to express diagnosability of
systems <cit.> in a general
asynchronous setting.

In the diagnosis process, faults of critical systems (referred as
plants) are handled by a dedicated module (the diagnoser)
running in parallel with the plant.

The diagnoser analyzes the observable information from the plant (made
available by predefined sensors), and is required to trigger suitable
alarms in correspondence to (typically unobservable) conditions of
interest (faults).

An alarm condition specifies the relation (delay) between a given
diagnosis condition and the raising of an alarm.

A plant  is diagnosable w.r.t. a given alarm condition
α, if there exists a diagnoser  which satisfies α
when  runs in parallel with .

Assume that the given set  of propositions is partitioned into a
set  of observable propositions and a set  of unobservable
propositions.

Two finite traces  and ' are observationally
equivalent iff the projections of
_(· P^ω) and
_('· (P')^ω) over  coincide, where
P is the last symbol of  and similarly P' is the last
symbol of '.

Given a pointed trace (,i), i is an observation point
of  if i>0 and
(i-1)∩≠(i)∩.

Then a plant  can be modeled as a finite Kripke structure
,_0,,, where  is
partitioned into internal transitions (,') where
()∩ = (')∩ and observable
transitions where ()∩≠(')∩.

A diagnoser  is modelled as a finite deterministic Kripke
structure over ' ⊇ (with '∩=∅).

In the behavioural composition of the plant  with , the
diagnoser only reacts to the observable transitions of the plant, that
is every transition of the diagnoser is associated with an observable
transition of the plant.

Simple  can express diagnosability with finite delay,
bounded delay, or exact
  delay <cit.>.

Here, we focus for simplicity on finite delay diagnosability.

Consider a diagnosis condition specified by a  formula β.

A plant  is finite delay diagnosable with respect to
β whenever for every pointed trace (,i) of  such
that (,i)β, there exists an observation point
k≥ i of  such that for all pointed traces (',i')
of  so that i' is an observation point of ' and
[0,k] and '[0,i'] are observationally equivalent, it
holds that (',j')β for some j'≤ i'.

Finite delay diagnosability w.r.t. β can be expressed in simple
 as follows, where
() (⊤∧⋁_p∈(p↔p).


    [ ∀^. (xβ→_(()∧∀^. {(()∧θ_(,)) →β}));           θ_(,)⋀_p∈_(p↔p) ∧ _(⊤∧⊤) ]




 §.§ Expressiveness issues



In this section, we present some results and conjectures about the
expressiveness comparison among , its simple fragment, and the
logics  and .

We also consider the logics for linear-time hyperproperties based on
the equal-level predicate whose most powerful representative is
.

Recall that the first-order fragment  of  is already
strictly more expressive than  <cit.> and, unlike
, its model-checking problem is decidable <cit.>.

Moreover, we show that  and its simple fragment represent an unifying
framework in the linear-time setting for specifying both
hyperproperties and the knowledge modalities of epistemic temporal
logics under both the synchronous and asynchronous perfect recall
semantics.

Our expressiveness results about linear-time hyper logics can be
summarized as follows.


  The following hold:


  *  is more expressive than , simple , and
  .

  * Simple  is more expressive than simple .

  * Simple  and  are expressively incomparable.

  * Simple  and  are expressively incomparable.




  We first show that there are hyperproperties expressible in simple
   but not in  and in .
  
  Given a sentence φ, the trace property denoted by
    φ is the set of traces  such that the singleton
  set of traces {} satisfies φ.
  
  It is known that  and  capture only regular
  trace properties <cit.>.
  
  In contrast simple  can express powerful non-regular trace
  properties.
  
  For example, consider the so called prefix property over
  ={p}: a trace  satisfies the prefix property if there
  exists a proper suffix ^i of  for some i>0 such
  that ^i=.
  
  This non-regular trace property can be
  expressed in  ∅ as follows:

  
  ∀_1. ∀_2. ⋀_p∈(p_1↔p_1) ∧ ∀_1. ∃^_2. ( ⋀_p∈(p[x_1] ↔ p[x_2])∧_2⊤)

   
  Next, we observe that  can be easily translated into ,
  since the pointer quantifiers of  correspond to the
  quantifiers of .
  
  Moreover, the predicate ≤' of , expressing that
    for the pointed traces (,i) and (',i')
  bound to  and ', =' and i≤ i',
  can be easily captured in .
  
  This is also the case for the equal-level predicate
  (,'), which can be expressed as
  {,'}(⊤∧'⊤).

  In Section <ref> we show that model checking
  of simple  is decidable.
  
  Thus, since model checking of both  and  are
  undecidable <cit.> and  subsumes
  , by the previous argumentation, the theorem follows.


It remains an open question whether  is subsumed by simple
.

We conjecture that neither  nor the fix-point calculus
 <cit.> (which captures both  and
 <cit.>) subsume simple .

The motivation for our conjecture is that  sentences consist of a
prefix of quantifiers followed by a quantifier-free formula where
quantifiers range over initial pointed traces
(,0).

Thus, unlike simple ,  cannot express requirements which
relate at some point in time an unbounded number of traces.

Diagnosability  (see Subsection <ref>) falls
in this class of requirements.

It is known that the following property is not definable in
 <cit.>: for some i>0, every trace in the given set
of traces does not satisfy proposition p at position i.

We conjecture that similarly to , such a property (and
diagnosability as well) cannot be expressed in .






Epistemic Temporal Logic  and its relation with
  .

The logic  <cit.> is a well-known extension of
 obtained by adding the unary knowledge modalities _a,
where a ranges over a finite set  of agents, interpreted under
the synchronous or asynchronous (perfect recall) semantics.

The semantics is given with respect to an observation map
:↦ 2^ that assigns to each agent a the set of
propositions which agent a can observe.

Given two finite traces  and ' and a∈, 
and ' are synchronously equivalent for agent a,
written ∼_a^sy', if the projections of  and
' over (a) coincide.

The finite traces  and ' are asynchronously
  equivalent for agent a, written ∼_a^as', if
the projections of _(a)(· P^ω) and
_(a)('· (P')^ω) over (a) coincide,
where P  is the last symbol of  and P' is the last symbol of
'.

For a set of traces  and a pointed trace (,i) over
, the semantics of the knowledge modalities is as follows,
where ∼_a is ∼_a^sy under the synchronous semantics, and
∼_a^as otherwise:

(,i) _,_a φ ⇔ for all pointed traces  (',i')  on 
  such that [0,i] ∼_a '[0,i'],  (',i')
_,φ.


We say that  satisfies φ w.r.t. the observation
  map , written _φ, if for all traces
∈, (,0) _,φ.

The logic  can be easily embedded into .

In particular, the following holds (for details, see
Appendix <ref>)


theoremtheoEmbeddingKnowledge
  
  Given an observation map  and a  formula ψ over
  , one can construct in linear time a ∅
  sentence φ_∅ and a  sentence φ such
  that φ_∅ is equivalent to ψ w.r.t.  under
  the synchronous semantics and φ is equivalent to ψ
  w.r.t.  under the asynchronous semantics.
  
  Moreover, φ is a simple  sentence if ψ is in
  the single-agent fragment of .






 
  

§ DECIDABILITY OF MODEL CHECKING AGAINST SIMPLE 


In this section, we show  that (fair) model checking against simple  is
decidable.

We first prove the result for the fragment ∅ of
simple  by a linear-time reduction to satisfiability of
full Quantified Propositional Temporal Logic (, for
short) <cit.>, where the latter extends  by
quantification over propositions.

Then, we show that (fair) model checking of simple  can be
reduced in time singly exponential in the size of the formula to
(fair) model checking of ∅.

We also provide optimal complexity bounds for model checking the
fragment ∅ in terms of a parameter of the given
formula called strong alternation depth.

For this, we first give similar optimal complexity bounds for
satisfiability of .

The syntax of  formulas φ over a finite set
 of atomic propositions is as follows: 


    φ ::= ⊤| p |φ|φ∨φ|φ|φ|φφ|φφ|∃ p .φ

 
where p∈ and ∃ p is the propositional existential quantifier.

A  formula φ is a sentence if each proposition
p occurs in the scope of a quantifier binding p and each temporal
modality occurs in the scope of a quantifier.

By introducing ∧ and the operators  (release, dual of
),  (past release, dual of ) and
∀ p (propositional universal quantifier), every 
formula can be converted into an equivalent formula in negation normal
  form, where negation only appears in front of atomic propositions.

 formulas are interpreted over pointed traces (,i) over
.

All  temporal operators have the same semantics as in .

The semantics of propositional quantification is as follows:


    (,i) ∃ p. φ ⇔  there is  a trace '   such that  =_∖{p}'  and  (',i) φ

 
where =_∖{p}' means that the
projections of  and ' over ∖{p}
coincide.

A formula φ is satisfiable if (,0)φ for
some trace .

We now give a generalization of the standard notion of alternation
depth between existential and universal quantifiers which corresponds
to the one given in <cit.> for .

This notion takes into account also the occurrences of temporal
modalities between quantifier occurrences, but the nesting depth of
temporal modalities is not considered (intuitively, it is collapsed to
one).

Formally, the strong alternation depth (φ) of a
 formula φ in negation normal form, is inductively
defined as follows, where an existential formula is a formula of the
form ∃ p. ψ, a universal formula is of the form
∀ p. ψ, and for a formula ψ, ψ denotes
the negation normal form of ψ:



  * For φ=p and φ= p for a given p∈:
  (φ) 0;

  * For φ=φ_1∨φ_2 and for
  φ=φ_1∧φ_2:
  (φ)max({(φ_1),(φ_2)});

  * For φ = ∃ p. φ_1: if there is no universal
  sub-formula ∀ψ of φ_1 such that
  (∀ψ)=(φ_1), then
  (φ)(φ_1). Otherwise,
  (φ)(φ_1)+1.

  * For φ = ∀ p. φ_1:
  (φ)(∃ p. φ_1).

  * For φ = φ_1 or
  φ = φ_1:
  (φ)(φ_1).

  * For φ = φ_1φ_2 or
  φ = φ_1φ_2: let h be the maximum over
  the strong alternation depths of the universal and existential
  sub-formulas of φ (where the maximum of the empty set is
  0).
  
  If the following conditions are met, then
  (φ) h; otherwise,
  (φ) h+1:
  
  
  * there is no existential or universal sub-formula ψ of
    φ_1 with (ψ)=h;
  
  * there is no universal sub-formula ψ of φ_2 with
    (ψ)=h;
  
  * no existential formula ψ with (ψ)=h occurs in
    the left operand (resp., right operand) of a sub-formula of
    φ_2 of the form ψ_1ψ_2, where
    ∈{,} (resp.,
    ∈{,}).
  

  * Finally, for φ = φ_1φ_2 or
  φ = φ_1φ_2:
  (φ)(φ).


 
For example, (∃(p∃ q))=0 and
(∃(∃ p q))=1.

The strong alternation depth of an arbitrary  formula
corresponds to the one of its negation normal form.

The strong alternation depth of a simple  formula is defined
similarly but we replace quantification over propositions with
quantification over trace variables.

For all n,h∈, (h,n) denotes a tower of exponentials of
height h and argument n: (0,n)=n and
(h+1,n)=2^(h,n).

The following result represents an improved version of Theorem 6
in <cit.> where h- is the class of languages
decided by deterministic Turing machines bounded in space by functions
of n in O((h,n^c)) for some constant c≥ 1.

While the lower bound directly follow from <cit.>, the
upper bound improves the result in <cit.>, since there,
occurrences of temporal modalities immediately preceding propositional
quantification always count as additional alternations (for details,
see Appendix <ref>).


  For all h≥ 0, satisfiability of  sentences with strong
  alternation depth at most h is h--complete.


Model checking against ∅.
We provide now linear-time reductions of model checking against
∅ to (and from) satisfiability of  which
preserve the strong alternation depth.

We start with the reduction of model checking ∅ to
 satisfiability.

theoremtheoFromEmptyGammaFragmentToQPTL
  
  Given a fair finite Kripke structure (,) and a
  ∅ sentence φ, one can construct in linear
  time a  sentence ψ (with the same strong alternation
  depth as φ) such that ψ is satisfiable if and only if
  (,)φ.



  Let = ,_0,,.
  
  In the reduction of model checking (,) against
  φ to  satisfiability we need to merge multiple traces
  into a unique trace where just a position is considered at any
  time.
  
  An issue is that the hyper quantifiers range over arbitrary pointed
  traces so that the positions of the different pointed traces in the
  current trace assignment do not coincide (intuitively, the different
  pointed traces are not aligned with respect to the relative current
  positions).
  
  However, this issue is resolved because the offsets between the
  positions of the pointed traces in the current trace assignment
  remain constant during the evaluation of the temporal modalities.
  
  In particular, assume that (,i) is the first pointed trace
  selected by a hyper quantifier during the evaluation along a path in
  the syntax tree of φ.
  
  We encode  by keeping track also of the variable 
  bound to (,i) and the -fair path of 
  whose associated trace is .
  
  Let (',i') be another pointed trace introduced by another
  hyper quantifier during the evaluation of φ bounding another
  variable .
  
  If i'<i, we consider an encoding of ' which is similar to
  the previous encoding but we precede it with a padding prefix
  of length i-i' of the form
  {_}^i-i'.
  
  The arrow → indicates that the encoding is along the
  forward direction.

  Now, assume that i'>i.
  
  In this case, the encoding of ' is the merging of two
  encodings over disjoint sets of propositions: one along the forward
  direction which encodes the suffix (')^i'-i and another
  one along the backward direction which is of the form
  {_}·ρ·{_}^ω, where ρ
  is a backward encoding of the reverse of the prefix of
  ' of length i'-i.
  
  In such a way, the encodings of the pointed traces later introduced
  in the evaluation of φ are aligned with the reference
  pointed trace (,i).
  
  Since the positions in the backward direction overlap some positions
  in the forward direction, in the translation, we keep track whether
  the current position refers to the forward or to the backward
  direction.
  
  The details of the reduction are 
  in Appendix <ref>.


By an adaptation of the known reduction of satisfiability of 
without past to model checking of  <cit.>,
we obtain the following result (for details, see also
Appendix <ref>).

theoremtheoFromQPTLtoEmptyGammaFragment
  
  Given a  sentence ψ over , one can build in
  linear time a finite Kripke structure _ (depending only on
  ) and a singleton-free ∅ sentence φ
  having the same strong alternation depth as ψ such that ψ
  is satisfiable iff (_)φ.


Hence, by
Theorems <ref>–<ref>,
we obtain the following result.


  For all h≥ 0, the fair model checking against
  ∅ with strong alternation depth at most h is
  h--complete.



Reduction to model checking against ∅.

We solve the fair model checking for simple  by a reduction to
fair model checking against the fragment ∅.

Our reduction is exponential in the size of the given sentence and is
an adaptation of the known reduction from model checking simple
 to model checking  <cit.>.

As a preliminary step, we first show, by an easy adaptation of the
standard automata-theoretic approach for  <cit.>, that
the problem for a simple  sentence φ can be reduced in
exponential time to the fair model checking problem against a
singleton-free sentence in the fragment Γ for some set
Γ of atomic propositions depending on φ.

For details, see Appendix <ref>.

propositionpropFormSimpleToProposition
  
  Given a simple  sentence φ and a fair finite Kripke
  structure (,) over , one can build in single
  exponential time in the size of φ, a fair finite Kripke
  structure (',') over an extension ' of  and
  a singleton-free Γ' sentence φ' for some
  Γ'⊆ ' such that
  (',')φ' if and only if
  (,)φ.
  
  Moreover, φ' has the same strong alternation depth as
  φ, |φ'|=O(|φ|), and
  |'|=O(||* 2^O(|φ|)).


Let us fix a non-empty finite set Γ⊆ of atomic
propositions.

We now show that fair model checking of the singleton-free fragment of
Γ can be reduced in polynomial time to fair model
checking of ∅.

We observe that in the singleton-free fragment of Γ,
when a pointed trace (,i) is selected by a pointed quantifier
∃^, then the positions of  which are
visited during the evaluation of the temporal modalities are all in
the (Γ,ω)-stutter factorization of  with the
possible exception of the position i chosen by
∃^.

Thus, given a set  of traces and a special proposition
∉, we define an extension
_Γ^() of the set
_Γ()={_Γ()|∈}.

Intuitively, we consider for each trace ∈, its
Γ-stutter trace _Γ() and the extensions of
_Γ() which are obtained by adding an extra
position marked by proposition # (this extra position does not
belong to the (Γ,ω)-stutter factorization of ).
Formally, _Γ^() is the smallest set
containing _Γ() and satisfying the following
condition:



  * for each trace ∈ with (Γ,ω)-stutter
  factorization {ℓ_k}_k≥ 0 and position
  i∈ (ℓ_k,ℓ_k+1) for some k≥ 0, the trace
  (ℓ_0)…(ℓ_k) ((i)∪{}) (ℓ_k+1) (ℓ_k+2)…∈_Γ^().



Given a singleton-free formula φ in Γ, we
denote by _(φ) the formula in ∅
obtained from φ by applying inductively the following
transformations:



  * the Γ-relativized temporal modalities are replaced with
  their ∅-relativized counterparts;

  * each formula ∃. ϕ is replaced with
  ∃. (_(ϕ)∧x);

  * each formula ∃^. ϕ is replaced with
  ∃^. (_(ϕ)∧x(∧ (⊤→)));



Intuitively, _(∃^. ϕ) states
that for the pointed trace (,i) selected by the pointed
quantifier, at most position i may be marked by the special
proposition #.

By the semantics of the logics considered, the following holds.


  Given a singleton-free sentence φ of Γ and a
  set  of traces, it holds that φ if and
  only if _Γ^()_#(φ).


Fix now a fair finite Kripke structure (,).

We first show that one can build in polynomial time a finite
Kripke structure (_Γ,_Γ) and a  formula
θ_Γ such that _Γ^((,))
coincides with the traces of (_Γ,_Γ) satisfying
θ_Γ (details are  in
Appendix <ref>).

propositionpropExtendedStutterTrace
  
  Given ∅≠Γ⊆ and a fair finite Kripke
  structure (,) over , one can construct in
  polynomial time a fair finite Kripke structure
  (_Γ,_Γ) and a  formula θ_Γ
  such that _Γ^((,)) is the set of
  traces ∈(_Γ,_Γ) so that
  θ_Γ.


Fix now a singleton-free sentence φ of Γ.

For the given fair finite Kripke structure (,) over
, let (_Γ,_Γ) and θ_Γ as in
the statement of Proposition <ref>.

We consider the ∅ sentence (φ)
obtained from _(φ) by inductively replacing (i)
each subformula ∃. ϕ of _(φ) with
∃. ((ϕ)∧θ_Γ), and (ii) each subformula ∃^. ϕ of
_(φ) with
∃^. ((ϕ)∧(⊤∧θ_Γ)).

In other terms, we ensure that in _(φ) the hyper
quantification ranges over traces which satisfy the  formula
θ_Γ.

By Remark <ref> and
Proposition <ref>, we obtain that
(,)φ if and only if
(_Γ,_Γ)(φ).

Thus, by Proposition <ref>, we obtain the
following.


  The fair model checking problem against simple  can be
  reduced in singly exponential time to fair model checking against
  ∅.














  
 

§ CONCLUSION


We have introduced  a novel hyper logic   which merges two
known asynchronous temporal logics for hyperproperties, namely
stuttering  and context .

Even though model checking of the resulting logic  is undecidable, we have
identified a useful fragment, called simple , that has a decidable model checking,
is strictly more expressive than  and than previously proposed
 fragments of asynchronous temporal logics for
hyperproperties with a decidable model checking. For the fragment 
∅ of simple , we have given optimal complexity bounds of fair model checking
in terms of the strong alternation depth of the given sentence. For arbitrary sentences in simple ,
fair model checking is reduced in exponential time to fair model checking of ∅. 
It is worth noting that simple  can express non-regular trace properties
over singleton sets of traces which are not definable in . An intriguing open
question is whether  can be embedded in simple .

In a companion paper <cit.> we study
asynchronous properties on finite traces by adapting simple  in prenex
form to
finite traces and past operators, and introduce practical
model-checking algorithms.







  plainurl
  

  
















§ PROOFS FROM SECTION <REF>




 §.§ Equally-expressive  extension of simple 


In this section, we show that the extension of simple  as defined at the end of Subsection <ref>
is not more expressive than simple . In the following,  a singleton-context formula is a
quantifier-free  formula
of the form ξ, where ξ  only uses singleton contexts  and temporal modalities with subscript ∅.
A singleton-context formula is simple if it is of the form ψ for some  formula ψ.
Thus, the considered extension of simple  is obtained by replacing simple singleton-context sub-formulas with arbitrary singleton-context sub-formulas.
Given two quantifier-free  formulas φ and φ', we say that φ and φ' are equivalent if
(i) φ and φ' use the same trace variables, and (ii) for each  trace assignment  whose domain contains the variables of φ,
(,)φ iff (,)φ'.
In order to show  that the considered extension of simple  has the same expressiveness as simple , it suffices to show the following result.

 Given a singleton-context  formula ξ, one can construct a Boolean combination φ of simple singleton-context  formulas and relativized propositions such that φ and ξ are equivalent.


For the proof, we need  additional definitions. Let Λ be a finite set whose elements are simple singleton-context formulas or relativized atomic propositions.
A guess for Λ  is a mapping :Λ↦{⊤,⊤} assigning to each formula in Λ a Boolean value (⊤ for true, and ⊤ for false). We denote by G_Λ the finite set of guesses for Λ.

Fix a singleton-context  formula ξ which is not simple.  We prove Proposition <ref> by induction on  the nesting depth of the context modalities in ξ.


For the base case, ξ does not contain context modalities. Let Λ be the set of relativized atomic propositions p occurring in ξ such that
≠. Then, the formula φ satisfying Proposition <ref> is given by


    φ⋁_∈ G_Λ(ξ()∧⋀_θ∈{θ∈Λ|(θ)=⊤}θ∧⋀_θ∈{θ∈Λ|(θ)=⊤}θ)


where ξ() is obtained from ξ by replacing all occurrences of the sub-formulas θ∈Λ in ξ with (θ). Note that
φ is a Boolean combination of simple singleton-context formulas and relativized propositions. Correctness of the construction follows from the fact that
by the semantics of , the position of the pointed trace assigned to a variable  distinct from  remains unchanged during the valuation of
the formula ξ within the singleton context .

For the induction step, assume that ξ contains singleton context modalities.
By the induction hypothesis, one can construct a formula ξ' which is a Boolean combination of simple singleton-context formulas and relativized propositions
such that ξ and ξ' are equivalent. Let Λ be the set consisting of the relativized atomic propositions p occurring in ξ' with ≠ which are not in scope of a context modality, and the sub-formulas of ξ' of the form θ such that ≠ (note that by hypothesis θ is a simple singleton-context formula).
Then, the formula φ satisfying Proposition <ref> is given by


    φ⋁_∈ G_Λ(ξ'()∧⋀_θ∈{θ∈Λ|(θ)=⊤}θ∧⋀_θ∈{θ∈Λ|(θ)=⊤}θ)


where ξ'() is obtained from ξ' by replacing all occurrences of the sub-formulas θ∈Λ in ξ' with (θ), and by removing the singleton context modality . Correctness
of the construction directly follows from the induction hypothesis and the semantics of .




 §.§ Proof of Theorem <ref>


*

We focus on the construction of the  sentence φ capturing the  formula
ψ under the asynchronous semantics w.r.t. the given observation map . The construction of the
 ∅ sentence φ_∅ capturing
ψ under the synchronous semantics w.r.t.  is similar. We inductively define a mapping _ assigning to each pair (ϕ,) consisting of a  formula ϕ and a trace variable ∈, a  formula _(ϕ,). Intuitively,
 is associated to the current evaluated pointed trace. The mapping _ is homeomorphic w.r.t. the Boolean connectives and the  temporal modalities
(i.e., (ϕ,)(ϕ,) for each ∈{,} and (ϕ_1  ϕ_2,)(ϕ_1,)  (ϕ_2,) for each ∈{∨,}) and is defined as follows when the given  formula is an atomic proposition or its root operator is a knowledge modality:


  * (p,)p;

  * (_aϕ,)∀^.  (θ_(a,,) →_(ϕ,)) where
≠ and


θ_(a,,)⋀_p∈(a)_(a)(p↔p) ∧ _(a)(⊤∧⊤)




Intuitively, θ_(a,,) asserts that for the pointed traces (,i) and (',i') bound to the trace variables
 and , respectively, [0,i] and [0,i'] are asynchronously equivalent for agent a w.r.t. the given observation map .
Note that _(ϕ,) is a simple  formula if ϕ is in the one-agent fragment of .
Let  be a set of traces, ∈, (,i) be a pointed trace over , and  be a trace assignment over  such that
∈() and ()= (,i). By a straightforward induction on the structure of a  formula φ, one can show that
(,i)_,ϕ if and only if (,) __(ϕ,). Hence, the desired  sentence φ
is given by ∀. _(ψ,) and we are done.




§ PROOFS FROM SECTION <REF>




 §.§ Automata for QPTL and Upper bounds of Theorem <ref>





  §.§.§ Automata for QPTL


In this section, we recall the classes of automata exploited in <cit.> for solving satisfiability of full  with past.
In the  standard automata-theoretic approach for  formulas φ in prenex  form <cit.>, first, one converts the quantifier-free part ψ of φ into an equivalent nondeterministic Büchi  automaton () accepting the set   (ψ) of traces satisfying ψ. Then, by using
the closure of   definable languages under projection and complementation, one obtains an   accepting (φ).
This approach would not work for arbitrary  formulas φ, where quantifiers can occur in the scope of both past and future temporal modalities. In this case, for a   subformula φ' of φ, we need to keep track of the full set _℘(φ') of pointed traces  satisfying φ, and not simply (φ'). Thus, the automata-theoretic approach proposed in <cit.>
is based on
a compositional translation of  formulas into a simple two-way extension of  , called
 simple two-way   (, for short) accepting languages of pointed traces.

Moreover, each step of the translation into   is based on an intermediate formalism consisting in  a two-way extension  of the class of (one-way) hesitant alternating automata (, for short) over infinite words introduced in <cit.>.



We now recall these two classes of automata. Moreover, for the class of two-way , we consider additional requirements which may be fulfilled by some states of the automaton. These extra requirements allow to obtain
a more fine-grained complexity analysis in the translation of two-way  into equivalent    , and they are important for obtaining an asymptotically optimal automata-theoretic approach for  in terms of the strong alternation depth of a  formula.




 <cit.>. An   over traces on 
is a tuple =Q,Q_0,,_-,_+, where  Q is a finite set of states, Q_0⊆ Q is a set of initial states, :Q×{→,←}× 2^→ 2^Q is a transition function, and _- and _+ are sets  of accepting states.
Intuitively, the symbols →
and ← are used to denote forward and backward  moves.
 A run of 
over a pointed trace (,i) is a pair r=(r_←,r_→) such that r_→=q_i,q_i+1… is an infinite sequence of states, r_←=q'_i,q'_i-1… q'_0 q'_-1 is a finite sequence of states, and: (i) q_i=q'_i∈ Q_0;
(ii) for each  h≥ i, q_h+1∈(q_h,→,(h)); and (iii)
 for each h∈ [0,i], q'_h-1∈(q'_h,←,(h)).

Thus, starting from the initial position i in the input pointed trace (,i), the automaton splits in two copies: the first one moves forwardly along the suffix of  starting from position i and the second one moves backwardly along the prefix (0)…(i).
The run r=(r_←,r_→) is accepting if q'_-1∈_- and r_→ visits infinitely often some state in _+. A pointed trace (,i) is accepted by  if there is an accepting run of  over (,i). We denote by _℘() the set of pointed traces accepted by  and by () the set of traces  such that (,0)∈_℘().



 Two-way  <cit.>.
Now, we recall the class of two-way .
For a set X, (X) denotes the set of positive Boolean
formulas over X built from elements in X using ∨ and ∧   (we also allow the formulas  and ).
 For a formula
θ∈(X), a model Y of θ is a subset Y
of X which satisfies θ. The model Y of θ is minimal
if no strict subset of Y satisfies θ.

A two-way    over traces on 
 is a tuple = Q,q_0,, _-,, where Q is a
finite set of states, q_0∈ Q is the initial state,  :
Q× 2^→({→,←}× Q) is a transition
function, _-⊆ Q is the backward acceptance condition, and  is a strata family encoding a particular kind of parity acceptance condition and imposing some syntactical constraints on the transition function .
Before defining  ,
 we give the notion of run which is independent of  and _-. We restrict ourselves to
  memoryless runs, in which the behavior of the automaton
  depends only on the current input position and current state. Since
  later we will deal only with parity acceptance conditions,
  memoryless runs are sufficient (see e.g. <cit.>).

Formally, given a pointed trace (,i)
and a state q'∈ Q, an (i,q')-run of  over  is a
directed graph V,,v_0 with set of vertices V⊆
(∪{-1})× Q and initial vertex v_0=(i,q'). Intuitively, a vertex (j,q) with j≥ 0 describes a copy of the automaton which is in state q and reads the j^th input position. Additionally, we require that the set of edges  is consistent with the transition function . Formally,
 for every vertex v=(j,q)∈ V such that j≥ 0, there is a minimal model
{(_1,q_1),…,(_n,q_n)} of (q,(j)) such that the set of successors of v=(j,q) is {(j_1,q_1),…,(j_n,q_n)}, where for all k∈ [1,n], j_k=j+1 if _k= →, and j_k=j-1 otherwise.

An infinite path π of a run is eventually strictly-forward whenever π has
a suffix of the form (i,q_1),(i+1,q_2),… for some i≥ 0.



Now, we formally define  and give the semantic notion of acceptance.
  is a strata family of the
form
={ρ_1,Q_1,_1,…,ρ_k,Q_k,_k},
where Q_1,…,Q_k is a partition of the set of states Q of , and for all i∈ [1,k],
ρ_i∈{-,,,} and _i⊆ Q_i, such that
_i=∅ whenever ρ_i∈{,-}. A stratum
ρ_i,Q_i,_i is called a negative stratum if ρ_i=-, a
transient stratum if ρ_i=, a Büchi 
stratum
(with Büchi acceptance condition _i) if ρ_i=, and a
coBüchi 
stratum (with coBüchi acceptance condition
_i) if ρ_i=.  Additionally, 
there is a
partial order ≤ on the sets Q_1,…,Q_k such that the
following holds:



  * Partial order requirement. Moves from states in Q_i lead to states in
  components Q_j such that
  Q_j≤ Q_i;  additionally, if Q_i belongs to a transient stratum, there are no
  moves from Q_i leading to Q_i.

  * Eventually syntactical requirement For all moves (,q') from states  q∈ Q_i such that q'∈ Q_i as well, the following holds:
  is ← if the
    stratum of Q_i   is negative, and  is
    → otherwise.
 
  * Each component Q_i satisfies one of the following two requirements:
 
  
  * Existential requirement: for all  states q_i∈ Q_i and input symbols a, if    (q,a) is rewritten in disjunctive normal form, then each conjunction contains at most one occurrence of a state in Q_i.
 
  * Universal requirement: for all  states q_i∈ Q_i and input symbols a, if    (q,a) is rewritten in conjunctive normal form, then each disjunction contains at most one occurrence of a state in Q_i.
 
 
  * Components of Büchi strata satisfy the existential requirement, while components of coBüchi strata satisfy the universal requirement.


The partial order requirement ensures
that every infinite path π of a run gets trapped in the component
Q_i of some  stratum.  The
eventually syntactical requirement  ensures that Q_i
belongs to a Büchi or coBüchi stratum and that π is
eventually strictly-forward. Moreover, the existential requirement for a component Q_i establishes that
from each state q∈ Q_i, at most one copy of the automaton is sent to the next input
symbol in component Q_i  (all the other copies move to states in strata with order lower than Q_i). Finally, the
 universal requirement corresponds to the dual of the existential requirement.
Note that transient components trivially satisfy both the existential and the universal requirement.[Is is worth noting that the existential and universal requirements are not considered in <cit.>. On the other hand, they are crucial in the automata-theoretic approach for .]

Now we define when a run is accepting.  Let π be an infinite path
 of  a  run,  ρ_i,Q_i,_i be
the Büchi or coBüchi stratum in which π gets trapped, and
 (π) be the states from Q that occur infinitely many
times in π. The path π is accepting whenever
(π)∩_i≠∅ if ρ_i= and (π)∩_i= ∅ otherwise (i.e. π satisfies the corresponding
Büchi or coBüchi requirement).
 A run is
accepting if: (i) all its infinite paths are accepting and (ii) for each
vertex (-1,q) reachable from the initial vertex, it holds that q∈_- (recall that _- is the backward acceptance condition of ).
 The
ω-pointed language _p() of  is the set
of pointed traces (,i)  such that there is an
accepting (i,q_0)-run of  on .


The dual automaton  of a two-way  =Q,q_0,,F_-, is defined
as =Q,q_0,,Q∖_-,, where
(q,a) is the dual formula of (q,a) (obtained from (q,a) by
 switching ∨ and ∧, and switching  and ),
and  is obtained from  by converting
a Büchi stratum ,Q_i,_i into the coBüchi stratum
,Q_i,_i and a coBüchi stratum ,Q_i,_i into
the Büchi stratum ,Q_i,_i.  By construction the dual automaton  of  is
still a two-way . Following standard arguments (see
e.g. <cit.>),  the following holds.


  The dual automaton  of a two-way   is a two-way  accepting the complement of
 _℘().


Note that   correspond to a subclass of two-way .


 An    can be  converted “on the fly” in linear time into a two-way  accepting _℘().


 Additional requirements on components of two-way . Let   =Q,q_0,,F_-, be a two-way .
 A component Q_i of  is globally nondeterministic if the following  inductively holds:
 
   
  * Q_i satisfies the existential requirement and Q_i is not a coBüchi component;
   
  * for each component Q_k distinct from Q_i such that there are moves from Q_k leading to Q_i (hence, Q_k>Q_i), (i) Q_k is globally nondeterministic, and (ii) for each q∈ Q_k and input symbol a, if
       (q,a) is rewritten in disjunctive normal form, then each conjunction contains at most one occurrence of a state in Q_i.
 


The previous requirement ensures that in each run r and for each input position ℓ, there is at most one copy of the automaton that is in some state
of Q_i reading position ℓ. A state of  is globally nondeterministic if it belongs to some globally nondeterministic component of .



 From two-way  to  <cit.>. Two-way  can be translated in singly exponential time
 into equivalent  <cit.>. The translation in <cit.>  is a  generalization of the Miyano-Hayashi
construction <cit.> (for converting by an exponential blowup a Büchi alternating automaton into an equivalent
 )  and exploits the so  called ranking construction <cit.> for converting in quadratic time
 a coBüchi alternating automaton  into an  equivalent Büchi alternating automaton. The translation can be easily adapted for handling
 globally nondeterministic components in two-way . Thus, we obtain the following result.

  
  Given a two-way  ,  one can construct “on the fly” and in singly
  exponential time a Büchi   accepting _℘() with
  2^O(n·log(n+ k)) states, where k is the number of states
  in the globally nondeterministic components of ,  and n is the number of remaining states of .





  §.§.§ Upper bounds of Theorem <ref>



In this section, in order to provide the upper bounds of Theorem <ref>, we first illustrate  a compositional translation of a  formula   into an equivalent  which improves the one given in <cit.>. There, occurrences of temporal modalities immediately preceding propositional quantification always count as additional alternations, and so they lead to an additional exponential blowup in the compositional translation.
 The relevant case in the translation is when the outermost operator of the currently processed sub-formula φ (assumed to be in negation normal form)  is a temporal modality (the other cases easily follow from the  closure of -definable pointed languages under union, intersection, and projection). This case is handled by first building a two-way   accepting _℘(φ) and then by applying Proposition <ref>.  The construction of   is obtained by a generalization of the standard linear-time translation of  formulas into Büchi alternating automata which exploits the (inductively built)   associated with the maximal universal and existential sub-formulas of φ.
 Formally, we establish the following result, where
for a     formula φ, we say that φ  is of universal-type if there is a universal sub-formula
ψ of the negation normal form of φ such that
( ψ)=(φ); otherwise, we say that φ is of existential-type.


Let φ be a   formula of existential-type (resp., of universal-type)  and h=(φ). Then, one can construct “on the fly” an   _φ accepting _℘(φ)   in time (h+1,O(|φ|)) (resp., (h+2,O(|φ|))).

 We assume without loss of generality that φ is in negation normal form.
The proof is given by induction on the structure of φ.  The base case  is trivial. For the induction step, we distinguish four cases depending on the type of root operator of φ (either positive  boolean connective, or existential quantifier, or universal quantifier, or temporal modality).



 Case 1:  φ is of the form φ=φ_1∧φ_2 or φ=φ_1∨φ_2. Assume that
  φ=φ_1∧φ_2 (the other case being similar).
  We use the fact that like Büchi nondeterministic automata,  are trivially and efficiently  closed under intersection. In particular, given
two    _1 and _2, one can construct “on the fly” and in time O(|_1||_2|) an 
accepting the language _℘(_1)∩_℘(_2).
  Since (φ)=max((φ_1),(φ_2)),  the result easily follows from the induction hypothesis. 












Case 2:  φ is an existential formula of the form φ=∃ p. φ'.
Hence, in particular, φ is  of existential-type.
Let h=(φ) and h'=(φ').
We observe that like Büchi nondeterministic automata,  are  efficiently  closed under projection. In particular, given
an    over traces and p∈, one can construct “on the fly” and in linear time an  
accepting the pointed language {(,i)  | there is  (',i)∈_℘()  such that '=_∖{p}}.
Thus, by applying the induction hypothesis, it follows that one can construct “on the fly” an   accepting _℘(φ) of size
(h',O(|φ'|)) if φ' is of existential-type, and of size (h'+1,O(|φ'|)) otherwise.
Since h'= h if φ' is of existential-type, and h'=h-1 otherwise (φ' is of universal-type), the result follows.



Case 3:  φ is a  universal formula of the form φ=∀ p. φ'.
Hence, in particular, φ is of universal-type.
Let h=(φ) and φ ' be the negation normal form of φ'.
We have that ( ∃ p. φ ')=h and _℘(∃ p. φ ')=_℘(φ). Hence, by Case 2, one can construct “on the fly” an   _φ
  of size (h+1,O(|φ|)) accepting _℘(φ). By Propositions <ref>, <ref>  and <ref>,  it follows that one
  can construct “on the fly” an   _φ
  of size (h+2,O(|φ|)) accepting _℘(φ). Hence, the result follows.



Case 4:  the root operator of φ is a temporal modality.
Let h=(φ) and
 P be the set of existential and universal sub-formulas of φ  which do not occur in the scope of a quantifier. If P=∅, then
φ is a  formula and h=0. In this case, by a straightforward adaptation of the standard translation of  into Büchi word automata <cit.>,  one can construct a    of size  2^O(|φ|) accepting _℘(φ). Hence, the result follows.

Assume now that P≠∅. Then, φ can be viewed as a  formula in negation normal form, written (φ), over the set of atomic propositions given by P∪.


Subcase 4.1: we first, assume that for each ψ∈ P, (ψ)<(φ). Hence, for all ψ∈ P,
(ψ)≤ h-1 and h≥ 1. Note that
φ is of existential-type.  Moreover, for each universal formula ∀ p. ξ∈ P, we have that
(∀ p. ξ)=(∃ p. ξ) and
_℘(∀ p. ξ)=_℘(∃ p. ξ), where ξ is the negation normal form
of ξ. Thus, since each existential formula is of existential-type,
 by applying the induction hypothesis, Proposition <ref> and the complementation result for two-way  (see Proposition <ref>), it follows that for each ψ∈ P, one can construct “on the fly” in time at most (h,O(|ψ|)), a two-way  _ψ accepting _℘(ψ). Then, by an easy generalization of the standard linear-time translation of  formulas into Büchi alternating word automata and by using the two-way  _ψ with ψ∈ P, we show that one can construct “on the fly”,
 in time (h,O(|φ|)), a two-way  _φ accepting _℘(φ).
 Intuitively, given an input pointed trace, each copy of  _φ keeps track of the current subformula of (φ) which needs to be evaluated. The evaluation simulates the semantics of  
 by using universal and existential branching, but when the current subformula ψ is in P, then the current copy of _φ activates a copy of _ψ in the initial state.

 Formally, for each ψ∈ P, let _ψ=Q_ψ,q_ψ,_ψ, _ψ^-, _ψ. Without loss of generality, we assume that the state sets of the two-way _ψ are pairwise distinct. Then, _φ=Q,q_0,,_-,, where:
 
 
   
  * Q = ⋃_ψ∈ PQ_ψ∪(φ), where (φ) is the set of subformulas of (φ);
   
  * q_0=φ;
   
  * The transition function  is defined as follows: (q,a) = _ψ(q,a) if q∈ Q_ψ for some ψ∈ P.
   If instead  q∈(φ), then (q,a) is inductively defined as follows:
   
     
  * (p,a) = if p∈ a, and (p,a) = otherwise (for all p∈∩(φ));
     
  * ( p,a) = if p∈ a, and ( p,a) = otherwise (for all p∈∩(φ));
     
  * (ϕ_1∧ϕ_2,a)=(ϕ_1,a)∧(ϕ_2,a) and (ϕ_1∨ϕ_2,a)=(ϕ_1,a)∨(ϕ_2,a);
     
  * (ϕ,a)=(→,ϕ) and (ϕ,a)=(←,ϕ);
      
  * (ϕ_1ϕ_2,a)=(ϕ_2,a)∨ ((ϕ_1,a)∧ (→,ϕ_1ϕ_2));
       
  * (ϕ_1ϕ_2,a)=(ϕ_2,a)∨ ((ϕ_1,a)∧ (←,ϕ_1ϕ_2));
       
  * (ϕ_1ϕ_2,a)=(ϕ_2,a)∧ ((ϕ_1,a)∨ (→,ϕ_1ϕ_2));
       
  * (ϕ_1ϕ_2,a)=(ϕ_2,a)∧ ((ϕ_1,a)∨ (←,ϕ_1ϕ_2));
      
  * for each ψ∈ P, (ψ,a)=_ψ(q_ψ, σ).
   
   
  * _-=⋃_ψ∈ P_ψ^-
   
  * = ⋃_ψ∈ P_ψ∪⋃_ϕ∈(φ){𝒮_ϕ}, where for each
   ϕ∈(φ), 𝒮_ϕ is defined as follows:
   
     
  * if ϕ has as root a past temporal modality, then 𝒮_ϕ is the negative stratum (-,{ϕ},∅);
     
  * if ϕ has as root the (future) until modality, then 𝒮_ϕ is the Büchi stratum (,{ϕ},∅);
          
  * if ϕ has as root the (future) release modality, then 𝒮_ϕ is the coBüchi stratum  (,{ϕ},∅);
     
  * otherwise, 𝒮_ϕ is the transient stratum given by (,{ϕ},∅).
   
 
 
 Finally, since h≥ 1 and the size of  the two-way  _φ is (h,O(|φ|)),
by applying Proposition <ref>, one can construct “on the fly” an    accepting _℘(φ) of size
(h+1,O(|φ|)). Hence, the result follows.



Subcase 4.2: for some ψ∈ P, (ψ)= (φ), and either φ=φ_1 and φ=φ_2.
This case easily follows from the induction hypothesis and the fact that given an   one can easily construct in linear time
two  _ and _ such that _℘(_)={(,i)| (,i+1)∈_℘()}
and _℘(_)={(,i)| i>0  and  (,i-1)∈_℘()}.



Subcase 4.3: for some ψ∈ P, (ψ)= (φ)=h, and either φ=φ_1φ_2 or φ=φ_1φ_2.
Let P_1 be the set of universal and existential sub-formulas of φ. Since ψ is a universal or existential sub-formula of φ and
(ψ)= (φ), by definition of the strong alternation depth, it follows that (i) φ and φ_2 are of existential-type, (ii) (φ_2)=(φ), and (iii) for each ψ_1∈ P_1, (ψ_1)<h. We focus on the case where φ= φ_1φ_2 (the case where φ=φ_1φ_2 is similar)
By the induction hypothesis, one can construct an  _2 in time (h+1,O(|φ|)) accepting _℘(φ_2)
 We distinguish two cases:
 
   
  * h=0: hence, P_1=∅ and φ_1 is a  formula.
   By an easy adaptation of the standard translation of  into Büchi word automata <cit.> and by exploiting the  _2 for the formula φ_2,  one can construct an   _φ  of size  2^O(|φ|) accepting _℘(φ).
     Intuitively, given an input pointed trace  (,i), _φ guesses a position j≥ i and checks that (,j)∈_℘() and for all k∈ [i,j), (,k)φ_1 as follows.
      Initially, _φ keeps track of both the guessed set Λ_0 of sub-formulas of φ_1 holding at the current position i, and the guessed state q of _2 which represents the state where the backward copy of _2 would be on reading the
      i^th position of  in some guessed accepting run of _2 over (,j). If j=i, then q needs to be some initial state of _2, and _2 simply simulates the behavior of _2 on (,i) and propagates the guesses about the sub-formulas of ψ_1 in accordance to the semantics of . Otherwise, _φ splits in two copies: the backward copy simulates the backward copy of _2 and deterministically checks that the initial guessed set Γ_0 of sub-formulas of φ_1 contains φ_1 and is consistent in the interval of positions [0,i], while the forward copy of _φ behaves as follows. In the first step, the forward copy of _φ moves to the same state (q,Γ_0), and after this step, such a copy starts to simulate  in forward-mode the backward copy of _2 until, possibly, a `switch' occurs at the guessed position j, where the forward copy of _φ simulates in a unique step from the current state some initial split of _2 in the backward and forward copy. In the phase before the switch, the current guessed set of sub-formulas always contains φ_1.
      After such a switch (if any), the forward copy of _φ simply simulates the forward copy of _2 and propagates the guesses about the sub-formulas of φ_1 in accordance to the semantics of . We use two flags to distinguish the different phases of the simulation (in particular, the initial phase and the switch phase). The acceptance condition is a  generalized Büchi condition which can be converted into a Büchi condition in a standard way.
   
  * h≥ 1: in this case, we construct a two-way  _φ accepting _℘(φ) as done for the subcase 4.1 but we replace
   the set P with the set P_1∪{φ_2}. Note that for each ψ∈ P_1, being (ψ)<h, the two-way  associated with formula ψ has size
   at most (h,O(|ψ|)). Moreover, let _φ_2 be the two-way  associated with the  _2 accepting _℘(φ_2).
   _φ_2 has size at most (h+1,O(|φ_2|)) and since it is the two-way  associated to an , it has just two strata: a negative existential stratum, say 𝒮_-, and a Büchi stratum (a Büchi stratum is always existential), say 𝒮_. Thus, applying the construction illustrated
   for the subcase 4.1, we have that the upper stratum 𝒮_φ of the two-way  _φ associated with the formula φ=φ_1φ_2  is a
   Büchi stratum consisting of the single state φ which is the initial state. Additionally, 𝒮_φ is the unique stratum from which it is possible to move to the strata of _φ_2, and for all input symbols a, if _φ(φ,a) is rewritten in disjunctive normal
   form, then each disjunction contains at most one state from 𝒮_- and at most one state from 𝒮_. In other terms, the strata
   𝒮_- and 𝒮_ are globally nondeterministic in _φ. Thus, _φ has at most  (h+1,O(|φ_2|))
   globally nondeterministic states while the number of remaining states is at most (h,O(|φ_1|)). By applying Proposition <ref>, one can construct “on the fly” an    accepting _℘(φ) of size
(h+1,O(|φ|)). Hence, the result follows.
 
 


Subcase 4.4: for some ψ∈ P, (ψ)= (φ), and either φ=φ_1φ_2 or φ=φ_1φ_2.  Since ψ is a universal or existential sub-formula of φ_1 or φ_2, by definition
of φ, ψ must be a universal formula. Hence, φ is of universal-type.
      Let φ ' be the negation normal form of φ'.
We have that (φ ')=h and _℘(φ ')=_℘(φ). Hence, by the subcase 4.3, one can construct “on the fly” an   _φ
  of size (h+1,O(|φ|)) accepting _℘(φ). By Propositions <ref>, <ref>  and <ref>, it follows that one
  can construct “on the fly” an   _φ
  of size (h+2,O(|φ|)) accepting _℘φ). Hence, the result follows. 



This concludes the proof of Theorem <ref>.


By exploiting Theorem <ref>, we can provide the upper bounds of Theorem <ref>.





For all h≥ 0, satisfiability of  sentences φ with strong alternation depth at most h  is in  h-.


We  observe that a  sentence is satisfiable iff it is valid. Thus, since a  sentence in negation normal form is a positive Boolean combination
of universal and existential sentences, it suffices to show the result for existential and universal  sentences φ:

  
  * φ=∃ p. φ': hence, φ is of existential-type. By Theorem <ref>, one can construct “on the fly” an   _φ accepting _℘(φ)   in time (h+1,O(|φ|)). We observe that an   can be trivially converted into a Büchi nondeterminstic automaton accepting the set of traces  such that (,0)∈_℘(). Thus, since  checking non-emptiness for Büchi nondeterministic automata is in , the result follows.
  
  * φ=∀ p. φ': since φ is a   sentence, we have that φ is satisfiable iff  ∃ p. φ is unsatisfiable.
  Thus, since (φ)=(∃ p. φ), this case reduces to the previous case.




 §.§ Detailed proof of Theorem <ref>


For a  formula φ and '⊆ with ' ={p_1,…, p_n}, we write ∃'.φ to mean
∃ p_1.…∃ p_n. φ.
Given a fair Kripke structure (,), a (,)-assignment is a partial mapping  over  assigning to each trace variable  in its domain
() a pair (,i) consisting of a -fair initial path of  and a position i≥ 0.


*
 
Let = ,_0,,. The high-level description of the  reduction of model checking (,) against φ
  to  satisfiability has been given in Section <ref>.  Here, we  provide the details of the reduction. We consider a new finite set ' of atomic propositions defined as follows:


    [                 ':= ⋃_∈_∪_∪{_,_}; _ := {p_,p_| p∈} and _ :={_,_|∈} ]


Let _:= {p_| p∈}, _:= {p_| p∈},
_ :={_|∈}, and
_ :={_|∈}.
Thus, we associate to each variable ∈ and atomic proposition p∈, two fresh atomic propositions p_ and
p_, and to each variable ∈ and state  of , two fresh atomic proposition _ and _. Moreover, for each ∈, _ and _ are exploited as padding propositions.



Encoding of paths and pointed paths of . For each ∈ and  path =_0,_1,… of , we denote by (,)   the trace over
_∪_ defined as follows for all i≥ 0:


    (,)(i):={(_i)_}∪{p_| p∈(_i)}

For each finite word  over , let (,) the trace over _∪_ given by w·{_}^ω, where |w|=|| and for each 0≤  i<||,
w(i)={(_i)_}∪{p_| p∈(_i)}.

Now, we define the forward and backward encodings of a path  of . For each k∈, the forward -encoding of  with offset k  is the trace over _∪_∪{_}, denoted by (,,k), defined as follows:


  
  * the projection of (,,k) over _∪_∪{_} is {_}^k·(,);
  
  * the projection of (,,k) over _∪_∪{_} is {_}^ω.



For each k>0,   the backward -encoding of  with offset k>0, is the trace over _∪_∪{_}, denoted by (,,k), defined as follows, where _≤ k^R denotes the reverse of the prefix (0)…(k-1) of  until position k-1:


  
  * the projection of (,,k) over _∪_∪{_} is (,^k);
  
  * the projection of (,,k) over _∪_∪{_} is {_}·(,_≤ k^R)·{_}^ω.









Claim 1.
  For all ∈, one can construct in linear time two  formulas θ(,→) and θ(,←) such that
  for all  pointed traces (,i) over ', we have:
 
   
  * (,i)θ(,→) iff there is a  -fair initial path  of  such that the projection of  over _∪_∪{_,_} is the forward -encoding of  for some offset k≥ 0.
   
  * (,i)θ(,←) iff there is a  -fair initial path  of  such that the projection of  over _∪_∪{_,_} is the backward -encoding of  for some offset k> 0.
 



We give the details on the construction of the  formula θ(,←) in Claim 1 (the construction of θ(,→) is similar).
For each state ∈,
  () denotes the set of successors of  in , while ^-1() denotes the set of predecessor of  in .
  The   formula θ(,←) is defined as follows:
 

    θ(,)   :=    ( (⊤)  ∧ _ ∧ _∧⋁_∈[ξ(,,→)∧⋁_'∈^-1()ξ(,',←)]   )
    ξ(,,→)    :=    _ ∧ ⋁_'∈ '_  ∧  ⋀_'∈('_→
          [⋀_p∈(')p_∧⋀_p∈∖(') p_∧⋀_”∈∖{'}”_∧⋁_”∈(') ”_] )
    ξ(,,←)    :=    _ ∧ _ ∧ ⋁_'∈_0 ('_∧_)   ∧   [_ → ⋀_q∈∪ q_]    ∧  
          ⋀_'∈( '_⟶[⋀_p∈(')p_  ∧⋀_p∈∖(') p_ ∧ _ ∧
          ⋀_”∈∖{'}”_ ∧ (  _∨⋁_”∈^-1(')”_) ] )




 We now extend the notions of backward and forward encodings of paths of  to pointed paths (,i)  of . For each k∈, the forward -encoding of (,i) with offset k is the pointed trace
given by ((,,k),i+k). We say that  the position i+k  is in forward mode in the encoding.  For each k>0,,   the backward -encoding of (,i) with offset k is the pointed trace
given by ((,,k),j), where j= i-k if i≥ k, and j=k-i otherwise. In the first case, we say that position j is in forward mode in the encoding, and the second case, we say that position j is in backward mode in the encoding.
Intuitively, when (,ℓ) is a backward or forward encoding of a pointed path (,i)   of , then  ℓ represents the position in the encoding associated to position i of .


Encoding of (,)-path assignments. Let  be a (,)-path assignment. A pointed trace (,i) over ' is a
forward encoding of  if for each ∈, the following holds, where _ denotes the projection of
 over _∪_∪{_,_}:


  
  * if ∉(), then _ is ∅^ω;
  
  * if ∈(), then (_,i) is a forward or backward encoding of
  () where i is in forward mode in the encoding.


When ()≠∅, we also consider the notion of a backward encoding (,i) of  which is defined as a forward encoding but we require that for each ∈(),
(_,i) is a  backward encoding of () where i is in backward mode in the encoding. Note that in this case, we have that
i≥ 1 holds.

Let  be a (,)-path assignment and   ' be the trace assignment over (,) obtained from 
in the obvious way. For each ℓ≥ 0, we write ^ℓ() to mean ^ℓ_(∅,)(') and ^ ℓ()
to mean ^ ℓ_(∅,)(').
By construction, we easily obtain the following result, where _→⋁_∈_ and
_←⋁_∈_.


Claim 2. Let  be a (,)-path assignment and ℓ≥ 0.

  
  * If (,i) is a forward encoding of , then:
  
  
  * (,i+ℓ) is a forward encoding  of ^ℓ();
  
  * if ℓ≤ i, then ^ ℓ()≠  iff  (,i-ℓ)_→. Moreover, if
   ^ ℓ()≠, then (,i-ℓ) is a forward encoding of ^ ℓ();
  
  * if ℓ> i, then ^ ℓ()≠  iff    (,ℓ-i)_←. Moreover, if
   ^ ℓ()≠, then (,ℓ-i) is a backward encoding of ^ ℓ().

  
  * If (,i) is a backward encoding of , then:
  
  
  * If ℓ<i, (,i-ℓ) is a backward encoding  of ^ℓ();
  
  * if ℓ≥ i, (,ℓ-i) is a forward encoding  of ^ℓ();
  
  * ^ ℓ()≠  iff   (,i+ℓ)_←. Moreover, if
   ^ ℓ()≠, then (,i+ℓ) is a backward encoding of ^ ℓ().




Reduction to  satisfiability.
 We  define by structural induction a mapping :{←,→}×∅→ associating to each pair (,ϕ) consisting of
   a direction ∈{←,→} and a ∅ formula ϕ over  and  a  formula (,ϕ) over '.
   Define '_:= _∨_∨{_,_}.


 
  * (,⊤)=⊤;
  
  * (←,p) = p_ for all p∈;
   
  * (→,p) = p_ for all p∈;
   
  * (,xψ) = _(, ψ), where
   _(, ψ) is obtained from (, ψ) by replacing each occurrence of _←
   (resp., _→) with _
   (resp., _);
  
  * (,ϕ)= (,ϕ);
   
  * (,ϕ_1∨ϕ_2)= (,ϕ_1)∨(, ϕ_2);
   
  * (←,ϕ)=  ((←,ϕ)∧⊤)  ∨  ((→,ϕ)∧⊤);
   
  * (→,ϕ)=  (→,ϕ);
  
  * (←,ϕ)= ((←, ϕ)∧_←);
  
  * (→,ϕ)= ((→, ϕ)∧_→)∨ [⊤∧ ((←, ϕ)∧_←)];
  
  * (←,ϕ_1   ϕ_2)= (←,ϕ_1)     (⊤∧(←,ϕ_2))   ∨

  (←,ϕ_1   ϕ_2)=
  [(⊤→(←,ϕ_1))∧(⊤∧(→,ϕ_1)   (→,ϕ_2)) ];
   
  * (→,ϕ_1   ϕ_2)= (→,ϕ_1)   (→,ϕ_2);
    
  * (←,ϕ_1  ϕ_2)= (←,ϕ_1)    ((←,ϕ_2)∧_←);
    
  * (→,ϕ_1   ϕ_2)= (→,ϕ_1)     ((→,ϕ_2)∧_→))   ∨

  (→,ϕ_1   ϕ_2)=
  [(→,ϕ_1) ∧( ⊤∧((←,ϕ_1)    ((←,ϕ_2)∧_←)))];
    
  * (←,∃. ϕ)= ∃ '_.    (θ(,←)∧(←,ϕ) ∧_∧_);
     
  * (→,∃. ϕ)= ∃ '_.    (θ(,→)∧(→,ϕ) ∧_∧ (⊤→_));
  
  * (←,∃^. ϕ)= ∃ '_.    (θ(,←)∧(←,ϕ) ∧_);
  
  * (→,∃^. ϕ)= ∃ '_.    ((→,ϕ) ∧ [θ(,←)∨
  (θ(,→)∧_)]);


where θ(,←) and θ(,→) are the  formulas of Claim 1. By construction  (,ϕ) has size linear in ϕ and has the same strong alternation depth as ϕ.
Moreover, (,ϕ) is a  sentence if ϕ is a ∅ sentence. Now, we prove that the construction is correct.
Given a ∅ formula ϕ such that () consists of all and only the trace variables occurring free in ϕ, we write
ϕ to mean that (',)_(,)ϕ, where  ' is the trace assignment over (,) obtained from 
in the obvious way. For a trace  over ', a variable ∈,   and a trace _ over
'_, we denote by [↦_] the trace  ' over ' such that
' =_'∖'_, and the projection of ' over '_ is _.
 For a ∅ sentence φ,  we show that
_∅ϕ⇔  (∅^ω,0) (→,φ) where (Π_∅)=∅.
The result directly follows from the following claim. 



Claim 3: let ∈{←,→}, ϕ be a ∅ formula, and
 be a (,)-assignment such that
 () contains all the trace variables occurring free in ϕ and = → if ()=∅. Then, for all
   encodings (,i) of  such that (,i) is forward encoding if =→, and a backward encoding otherwise, the following holds:

ϕ⇔  (,i) (,ϕ). 



The proof of Claim 3 is by structural induction on ϕ. When ϕ is a trace-relativized atomic proposition, the result directly follows
from the definition of the map  and the notion of an encoding (,i) of Π.  The cases for the boolean connectives directly follow from the induction hypothesis, while the cases relative to the temporal modalities  easily follow from the induction hypothesis, Claim 2 in the proof of Theorem <ref>, and the definition of the map . For the other cases, the ones relative to the hyper quantifiers,  we proceed as follows:


 
  * ϕ= ∃. ϕ': we focus on the case, where =← (the other case being similar). By hypothesis, (,i) is a backward encoding of  and ()≠∅. Hence, it holds that i≥ 1.
For the implication  ϕ⇒  (,i) (←,ϕ), assume that
ϕ. Hence, there exists a -fair initial path  of  such that
[↦ (,0)]ϕ'. Since i≥ 1, by construction, the trace _ over '_ given by   ((,,i),i) is the backward
-encoding of (,0) where i is in backward mode in the encoding.
Hence, the trace ' given by [↦_] is a backward encoding of [↦ (,0)].
By the induction hypothesis, (',i) (←,ϕ'). Moreover, by construction and Claim 1,
    (_,i) θ(,←), _∉_(i) and
  _∈_(i+1). Hence, by definition of (←,∃. ϕ'),
  we obtain that  (,i) (←,ϕ).

For the converse implication, assume that (,i) (←,ϕ).
By definition of (←,∃. ϕ') and  Claim 1, there exists a trace
_ over '_ such that _ is the
 backward -encoding (,,k) of some  -fair initial path  of  for some offset k>0. Moreover,
 (',i)ϕ', where ' is given by [↦_],
  _∉_(i) and
  _∉_(i+1). This means that the offset k is exactly i. Hence,
  ((,,i),i) is the backward
-encoding of (,0) where i is in backward mode in the encoding, and ' is a backward encoding
of  [↦ (,0)]. Thus, by the induction hypothesis, the result directly follows.

  * ϕ= ∃^. ϕ': we focus on the case, where =→ (the other case being similar). By hypothesis, (,i) is a forward encoding of .
For the implication  ϕ⇒  (,i) (←,ϕ), assume that
ϕ. Hence, there exists a -fair initial path  of  and a position ℓ≥ 0 such that
[↦ (,ℓ)]ϕ'. Let (_,i) be the trace over '_ defined as follows:

  
  * if ℓ≤ i: we set (_,i) to ((,,i-ℓ),i) which by construction is the forward
-encoding of (,ℓ). By construction and Claim 1, (_,i)θ(,→)∧_;
  
  * if ℓ> i: we set (_,i) to ((,,ℓ-i),i) which by construction is the backward
-encoding of (,ℓ) where i is in forward mode in the encoding. By construction and Claim 1, (_,i)θ(,←).

Hence, the trace ' given by [↦_] is a forward encoding of [↦ (,ℓ)].
By the induction hypothesis, (',i) (←,ϕ'). Hence, by definition of (→,∃^. ϕ'),
  we obtain that  (,i) (→,ϕ).

For the converse implication, assume that (,i) (→,ϕ).
By definition of (→,∃. ϕ') and  Claim 1, there exists a  -fair initial path  of  and a trace
_ over '_ such that (',i)ϕ', where ' is given by [↦_] and
 one of the following holds:

  
  * _ is the forward
-encoding     (,,k) of   for some offset k≥ 0 and _∉_(i). It follows that k≤ i and (_,i) is the
  forward -encoding of the pointed path (,i-k).
  
  * _ is the backward
-encoding     (,,k) of   for some offset k> 0.
Hence, (_,i) is
the backward -encoding of the pointed path (,i+k) where i is in forward mode in the encoding.

Hence, for some ℓ≥ 0, '=[↦_] is a forward encoding
of [↦ (,ℓ)]. Thus, being (',i)ϕ',  by the induction hypothesis, the result directly follows.


This concludes the proof of Claim 3 and  Theorem <ref> too.
 








 §.§ Proof of Theorem <ref>


*
Without loss of generality, we only consider well-named  formulas,   formulas where each quantifier introduces a different proposition.
Moreover, we can assume that  is the set of all and only the propositions occurring in the given  sentence.
 Let '=∪{,}, where  and  are fresh propositions, and fix an ordering {p_1,…, p_n} of the propositions in .
First, we encode a trace  over   by a trace () over ' defined as follows: ():=_0 ·_1 ·…, where
for each i≥ 0,  _i (the encoding of the i^th symbol of ) is the finite word over 2^' of length n+1 given by P_0 P_1,… P_n, where
(i) for all k∈ [1,n],  P_k= {p_k} if p_k∈(i), and P_k=∅ otherwise, and (ii) P_0= {} if i>0 and P_0={,} otherwise.
Note that proposition  marks the first position of ().
 Then, the finite Kripke structure   _= ,_0,, over ' has size linear in || and it is constructed in such a way that its set of traces (_) is the set of the encodings of the traces over .  Formally, _ is defined as follows:
 

  
  * ={p_h,p_h| h∈{1,…,n}}∪{,} and _0 = {};
  
  *  consists of the edges (p_k,p_k+1), (p_k,p_k+1),
  (p_k,p_k+1) and (p_k,p_k+1) for all k∈ [1,n-1], and the edges
  (,p_1), (,p_1), (p_n,), and (p_n,) where ∈{,}.
  
  * ()={}, ()={,}, and  (p_k)={p_k} and (p_k)=∅ for all k∈ [1,n].


Let Λ be the set of pairs (h,ψ) consisting of a natural number h∈ [0,n] and
 a well-named  formula ψ over  such that there is no quantifier in ψ binding proposition p_h if h≠ 0,
and ψ is a sentence iff h=0. We inductively define a mapping assigning to each pair (h,ψ)∈Λ a
 singleton-free ∅ formula (h,ψ) over ' and ={_1,…,_n} (intuitively, if h≠ 0, then p_h represents the currently quantified proposition):


 
  * (h,⊤)=⊤;
  
  * (h,p_i) = ^i p_i_h for all p_i∈;
  
  * (h,ψ)= (h,ψ);
   
  * (h,ψ_1∨ψ_2)= (h,ψ_1)∨(h,ψ_2);
   
  * (h,ψ)= ^n+1(h,ψ);
    
  * (h,ψ)= ^n+1(h,ψ);
   
  * (h,ψ_1  ψ_2)= (_h→(h,ψ_1))   ((h,ψ_2)∧_h);
    
  * (h,ψ_1  ψ_2)= (_h→(h,ψ_1))   ((h,ψ_2)∧_h);

   
  * [ (h,∃ p_k.ψ) =
  ∃^ _k.  ((k,ψ)  ∧(_h∧_k∧   
∃^ _k.  ((k,ψ)  ∧(⋀_j∈ [1,n]∖{k}(p_j_h↔p_j_k))
       if  h ≠ 0
∃ _k.  (k,ψ)
          otherwise ]


By construction,  (h,ψ) has size linear in ψ and has the same strong alternation depth as ψ.
Moreover, (h,ψ) is a ∅ sentence iff ψ is a  sentence. Now we show that the construction is correct.
A  (_)-assignment is a mapping  :→(_).
For all i≥ 0, (_)-assignments , and ∅ formulas φ over ', we write
(,i)φ to mean that (_i,)_(_)φ, where _i is the (pointed)
trace assignment over (_) assigning to each trace variable ∈, the pointed trace ((),i).
Note that for each  sentence ψ over , ψ is satisfiable if for all traces , (,0)ψ.
Thus, correctness of the construction directly follows from the following claim,  where
for each i≥ 0,   ℘(i):= i·(n+1).  Intuitively, ℘(i) is the -position associated with the '-encoding of the position i of a trace over .


Claim. Let (h,ψ)∈Λ. Then, for all pointed traces (,i) over  and (_)-assignments 
  such that (_h) = () if h≠ 0, and i=0 if h=0, the following holds:


    (,i) ψ⇔ (,℘(i)) (h,ψ)


 The claim is proved  by structural induction  on ψ. The cases for the boolean connectives  easily follow from the induction hypothesis. For the other cases, we proceed as follows:


   
  * ψ = p_j for some p_j∈: in this case h≠ 0 (recall that (h,ψ)∈Λ). Then, we have that
  (,i)  p_j  ⇔ p_j∈(i) ⇔  p_j∈()(℘(i)+j) ⇔
  p_j∈(_h) (℘(i)+j) ⇔ (, ℘(i)) ^j p_jx_h
  ⇔ (, ℘(i)) (h,p_j).
 Hence, the result follows.
  
  * ψ =ψ': hence, h≠ 0. We have that
  (,i) ψ'  ⇔ (,i+1)ψ' ⇔ (by the induction hypothesis)
   (, ℘(i+1)) (h,ψ') ⇔ (since ℘(i+1)= ℘(i)+n+1)
   (, ℘(i)) ^n+1(h,ψ') ⇔ (,℘(i))(h,ψ').
 Hence, the result follows.
 
  * ψ = ψ': similar to the previous case.
 
  * ψ =ψ_1ψ_2: hence, h≠ 0. We have that
  (,i) ψ_1 ψ_2  ⇔
  there is j≥ i such that
 (,j)ψ_2 and (,ℓ) ψ_1 for all i≤ℓ<j ⇔
 (by the induction hypothesis)
   there is j≥ i such that
 (, ℘(j)) (h,ψ_2) and (, ℘(ℓ)) (h,ψ_1) for all i≤ℓ<j ⇔
 there is j'≥℘(i) such that (,j') (h,ψ_2) and ∈(x_h)(j'), and for all
 ℘(i)≤ℓ'<j' such that ∈(x_h)(ℓ'), (,ℓ') (h,ψ_1)
 ⇔ (,℘(i)) (h,ψ_1ψ_2).
  Hence, the result follows.
 
  * ψ =ψ_1ψ_2: similar to the previous case.
  
  * ψ= ∃ p_k. ψ' and h≠ 0: by hypothesis, k≠ h.
For the implication, (,℘(i)) (h,ψ) ⇒ (,i) ψ, assume that
(,℘(i)) (h,ψ). By definition of (h,∃ p_k. ψ') and since  marks the first position
of the encoding of a trace over ,  it easily follows that there exists  a pointed  trace over  of the form (',i) such that '=_∖{p_k}
and ([x_k ←(')], ℘(i))(k,ψ'). Since (k,ψ')∈Λ, by the induction hypothesis,
it follows what  (',i) ψ'.
  Thus,   being '=_∖{p_k}, we obtain that  (,i) ψ.


The converse implication  (,i) ψ⇒  (Π,  ℘(i))(h,ψ) is similar, and we omit the details here.

  * ψ= ∃ p_k. ψ' and h= 0: hence, ψ and (0,ψ) are sentences.
We have that
  (,0) ∃ p_k. ψ'  ⇔ (ψ is a  sentence) for some trace ' over , (',0)ψ' ⇔ (by the induction hypothesis)
   ([→(')], ℘(0)) (k,ψ') ⇔ (by definition of (0,∃ p_k. ψ'))
   (, ℘(0)) (0,∃ p_k. ψ').


This concludes the proof of Theorem <ref>.
  



 §.§ Proof of Proposition <ref>


In order to prove Proposition <ref>, we need some
preliminary results.

Recall that a Nondeterministic Büchi Automaton over words ( for short) is a tuple
=Σ,Q,Q_0,Δ,, where Σ is a finite
alphabet, Q is a finite set of states, Q_0⊆ Q is the set
of initial states, Δ⊆ Q×Σ× Q is the
transition relation, and ⊆ Q is the set of
accepting states. Given a infinite word w over Σ, a
run of  over w is an infinite sequence of states
q_0,q_1,… such that q_0∈ Q_0 and for all i≥ 0,
(q_i,w(i),q_i+1)∈Δ.

The run is accepting if for infinitely many i, q_i∈.  The
language () accepted by  consists of the infinite words
w over Σ such that there is an accepting run over w.

Fix a non-empty set Γ of  formulas over .

The closure (Γ) of Γ is the set of  formulas
consisting of the formulas ⊤, ⊤, the  sub-formulas of the formulas θ∈Γ, and
the negations of such formulas (we identify θ with θ).

Note that Γ⊆(Γ).

Without loss of generality, we can assume that ⊆Γ.

Precisely,  can be taken as the set of propositions occurring in
the given simple  sentence and (Γ) contains all the
propositions in  and their negations.

For each formula θ∈(Γ)∖, we introduce a
fresh atomic proposition not in , denoted by
(θ). Moreover, for allowing a uniform notation, for each
p∈, we write (p) to mean p itself.

Let _Γ be the set  extended with these new
propositions.

By a straightforward adaptation of the well-known translation of
 formulas into equivalent  <cit.>, we
obtain the following result, where for a trace _Γ over
_Γ, (_Γ)_ denotes the projection of _Γ over .



  
  Given a finite set Γ of  formulas over , one can
  construct in single exponential time an  _Γ
  over 2^_Γ with 2^O(|_Γ|) states satisfying
  the following:
  
  
  * let _Γ∈(_Γ): then for all i≥ 0 and
    θ∈(Γ), (θ)∈_Γ(i) iff
    ((_Γ)_,i)θ.
  
  * for each trace  over ,
    there exists _Γ∈(_Γ) such that = (_Γ)_.



 Here, we construct a generalized 
  _Γ satisfying Properties (1) and (2) of
  Proposition <ref> which can be converted in linear
  time into an equivalent . Recall that a generalized
   is defined as an  but the acceptance condition
  is given by a family ={_1,…,_k} of sets
  of accepting states. In this case, a run is accepting if for each
  accepting component _i∈, the run visits
  infinitely often states in _i.

The generalized  _Γ = 2^_Γ,Q,Q_0,Δ,  is defined as follows.
Q is the set of atoms of Γ consisting of the maximal  propositionally consistent subsets A of (Γ).
Formally, an atom A of Γ is a subset of (Γ)   satisfying the following:
 
 
  * ⊤∈ A
  
  * for each θ∈(Γ), θ∈ A iff θ∉ A;
    
  * for each θ_1∨θ_2∈(Γ), θ_1∨θ_2∈ A iff {θ_1,θ_2}∩ A≠∅.


The set Q_0 of initial states consists of the atoms A of Γ such that ⊤∈ A.
For an atom A, (A) denotes the subset of propositions in _Γ associated with the formulas in A, i.e.
(A){(θ)|θ∈ A}.
The transition relation Δ captures the semantics of the next and previous modalities  and the local fixpoint characterization of the until and since  modalities.
Formally, Δ consists of the transitions of the form (A,(A),A') such that:
 
 
  * for each θ∈(Γ), θ∈ A iff θ∈ A';
 
  * for each θ∈(Γ), θ∈ A' iff θ∈ A;
  
  * for each θ_1θ_2∈(Γ), θ_1θ_2∈ A iff either θ_2∈ A, or θ_1∈ A  and θ_1θ_2∈ A';
  
  * for each θ_1θ_2∈(Γ), θ_1θ_2∈ A' iff either θ_2∈ A', or θ_1∈ A'  and θ_1θ_2∈ A.

Finally, the generalized Büchi acceptance condition is used for ensuring the fulfillment of the liveness requirements θ_2 in the until sub-formulas θ_1θ_2 in Γ. Formally, for each θ_1θ_2∈(Γ),  has a component
consisting of the atoms A such that either (θ_1θ_2)∈ A or θ_2∈ A.


Let _Γ∈(_Γ). By construction, there is an accepting infinite sequence of atoms ρ=A_0 A_1…  such that for all i≥ 0, _Γ(i)=(A_i). Let  be the projection of _Γ over  (note that A_i∩ = (i) for all i≥ 0).
By standard arguments (see <cit.>), the following holds: for all i≥ 0 and θ∈(Γ), θ∈ A_i (hence, (θ)∈_Γ(i)) if and only if (,i)θ.
Hence, Property (1) of Proposition <ref> follows.

For Property (2), let  be a trace over  and let ρ= A_0 A_1… be the infinite sequence of atoms defined
as follows for all i≥ 0: A_i={θ∈(Γ)| (,i)θ}. By construction and the semantics of ,
ρ is an accepting run of _Γ over the word _Γ= at(A_0) at(A_1)…. Moreover,  coincides with the projection of _Γ over . Hence, the result follows.



Let = ,_0,, be a finite Kripke structure over  and ⊆.

Next, we consider the synchronous product of the fair Kripke structure
( , ) with the 
_Γ = 2^_Γ,Q,Q_0,Δ, over
2^_Γ of Proposition <ref> associated with
Γ.

More specifically, we construct a Kripke structure _Γ over
_Γ and a subset _Γ of _Γ-states such that
(_Γ,F_Γ) is the set of traces
_Γ∈(_Γ) whose projections over  are in
(,).

Formally, the Γ-extension of (,) is the fair
Kripke structure (_Γ,_Γ) where
_Γ=_Γ,_0,Γ,_Γ,_Γ and
_Γ are defined as follows:



  * _Γ is the set of tuples
  (,B,q,ℓ)∈× 2^_Γ× Q×{1,2} such
  that (s)= B∩;

  * _0,Γ= _Γ∩ (_0× 2^_Γ×
  Q_0×{1});

  * _Γ consists of the following transitions:
  
  
  * ((,B,q,1),(',B',q',ℓ)) such that (,')∈,
    (q,B,q')∈Δ, and ℓ=2 if ∈ and ℓ=1
    otherwise;
  
  * ((,B,q,2),(',B',q',ℓ)) such that (,')∈,
    (q,B,q')∈Δ, and ℓ=1 if q∈ and ℓ=2
    otherwise.
  

  * for each (,B,q,ℓ)∈_Γ, _Γ((s,B,q,ℓ))=B;

  * _Γ={(,B,q,2)∈_Γ| q∈}.


By construction and Proposition <ref>(2), we
easily obtain the following result.



  
  For each trace _Γ over _Γ,
  _Γ∈(_Γ,_Γ) if and only if
  _Γ∈(_Γ) and (_Γ)_∈(,). Moreover,
  for each ∈(,), there exists
  _Γ∈(_Γ,_Γ) such that (_Γ)_ =.



We can now provide a proof of Proposition <ref>.

*

Let φ be a  sentence over  and (,)
be a fair finite Kripke  structure (,) over .
Then, there is a finite set Γ_0 of  formulas  such that
φ is in the fragment Γ_0.
Let Γ be the set of  formulas consisting of the formulas
in Γ_0 and the  formulas ψ such that
xψ is a sub-formula of φ for some variable .
Define ', Γ'⊆', (','), and φ' as follows:

 
  * '_Γ (recall that _Γ=∪{(θ)|θ∈Γ})
 and Γ' is the _Γ-counterpart of Γ_0, Γ'{(θ)|θ∈Γ_0};
 
  * (',') (_Γ,_Γ), where
   (_Γ,_Γ) is the Γ-extension of (,);
 
  * φ'(φ)  where the mapping  replaces (i) each sub-formula
    xψ of φ with its propositional version
    (ψ), and (ii) each Γ_0-relativized temporal modality  with its
    Γ'-relativized version. Note that (φ) is a singleton-free Γ' formula
    where Γ' is propositional (in particular, Γ'⊆') and has the same strong alternation
    depth as φ.
 

It remains to show that the construction is correct, (_Γ,_Γ)(φ) iff
  (,)φ. Let Λ be the set of formulas ϕ in the
fragment  Γ_0 such that for each sub-formula xψ of ϕ,
it holds that ψ∈Γ. Moreover, for a trace assignment _Γ over
 (_Γ,_Γ), the -projection of
 _Γ, written
 (_Γ)_, is the trace assignment with domain
 () obtained from
  by replacing each pointed trace  (), where ∈() and
 () is of the form (_Γ,i),
 with ((_Γ)_,i).  Note that by Proposition <ref>,
 (_Γ)_ is a trace assignment over (,).
Correctness of the construction directly follows from the following claim.


Claim. Let ϕ∈Λ and _Γ be a trace assignment over (_Γ,_Γ).
Then:


    _Γ_(_Γ,_Γ)(ϕ)iff(_Γ)__(,)ϕ


The claim is proved by a structural induction on ϕ∈Λ. The cases where the root modality of ϕ is a Boolean connective  directly follow from the induction hypothesis. For the other cases, we proceed as follows.

  
  * ϕ= xψ, where ψ∈Γ. Hence, (ϕ)= (ψ). Let _Γ()=(_Γ,i).
  We have that (_Γ)_()=((_Γ)_,i). By Propositions <ref> and <ref>,
  (ψ)∈_Γ(i) iff
    ((_Γ)_,i)ψ. Hence, the result follows.
  
  * The root modality of ϕ is a Γ_0-relativized temporal modality. Assume  that
  ϕ = ϕ_1 _Γ_0ϕ_2 (the other cases being similar). Then, (ϕ)= (ϕ_1) _Γ'(ϕ_2) (recall that
  Γ'= {(θ)|θ∈Γ_0} and Γ_0⊆Γ).  By Propositions <ref> and <ref>, for each pointed trace (_Γ,i) over (_Γ,_Γ) and θ∈Γ_0, it holds that
  (θ)∈_Γ(i) iff
    ((_Γ)_,i)θ. By construction, it follows that _(Γ_0,)((_Γ)_)
    is the -projection of _(Γ',)(_Γ). Hence, by the semantics of  and the induction hypothesis, the result follows.
  
  * ϕ = ∃. ϕ'. Hence, (ϕ)= ∃. ϕ'. By Proposition <ref>, for each trace ∈(,),
   there exists
  _Γ∈(_Γ,_Γ) such that (_Γ)_ =. Hence, the result easily follows from the induction hypothesis.
  
  * ϕ = ∃^. ϕ': this case is similar to the previous one.






 §.§ Proof of Proposition <ref>


*

Let =,_0,,.
Intuitively, the Kripke structure _Γ is obtained from
  by adding edges which are summaries of finite paths  of  where either the propositional valuation in Γ
 changes only at the final state of , or the propositional valuation in Γ does not change along .
 Formally, let _Γ() and _Γ(,) be the
 sets of state pairs in  defined as follows:
 
 
  * _Γ() consists of the pairs (,')∈×
   such that ()∩Γ≠(')∩Γ and there is a
   finite path of  of the form ·ρ·' such that
   ()∩Γ= (ρ(i))∩Γ for all 0≤ i<|ρ|.
 
  * _Γ(,) is defined similarly but, additionally, we
   require that the finite path ·ρ·' visits some
     state in .
 


Intuitively, _Γ() keeps track  of the initial and final states of the finite paths
 of  with length at least 2 where the propositional valuation in Γ changes only at the final state of the finite path.
 Additionally, _Γ(,) considers only those finite paths which visit  some state in .
 Moreover, let ^_Γ() and ^_Γ(,) be the
 sets of state pairs in  defined as follows:
 

  * ^_Γ() consists of the pairs (,')∈×
   such that ()∩Γ = (')∩Γ and there is a
   finite path of  of the form ·ρ·' such that
   ()∩Γ= (ρ(i))∩Γ for all 0≤ i<|ρ|.
 
  * ^_Γ(,) is defined similarly but, additionally, we
   require that the finite path ·ρ·' visits some
   accepting state in .
 


Thus, ^_Γ() keeps track  of the initial and final states of the finite paths
 of  with length at least 2 where the propositional valuation in Γ does not change.
 Additionally, ^_Γ(,) considers only those finite paths which visit  some state in .
 The finite sets _Γ(), _Γ(,), ^_Γ(), ^_Γ(,)  can be easily
 computed in polynomial time by standard closure algorithms. By
 exploiting these finite sets, we define
 the finite Kripke structure _Γ=_Γ,_Γ,0,_Γ,_Γ and the set _Γ⊆_Γ as follows.
 
 

  * _Γ is given by × 2^{,} and
  _Γ,0 is the set of states of the form (,∅) for some ∈_0.

  * _Γ consists of the edges ((,T),(',T')) such
  that one of the following holds:
  
  
  * or (,')∈∪_Γ(), ∉ T', and (∈ T'
    iff '∈);
  
  * or (,')∈_Γ(,), ∉ T', and ∈ T';
  
  * or (,')∈^_Γ(), ∉ T, ∈ T', and (∈ T'
    iff '∈);
  
  * or (,')∈^_Γ(,), ∉ T, ∈ T', and ∈ T'.
   
 
  * _Γ(,T)=()∪{} if ∈ T, and _Γ(,T)=() otherwise;
 
  * _Γ is the set of _Γ-states (,T) such that ∈ T.
 



Intuitively, proposition # marks only the -states which are targets of pairs in ^_Γ()∪^_Γ(,),
while the flag  marks either the states in  which are targets of -edges, or the -states which are targets
of pairs in _Γ(,)∪^_Γ(,). We say that
a trace  over ∪{} is well-formed if one of the following conditions holds:
  
  
  * or  is a Γ-stutter free trace over  (_Γ()=);
  
  * or there is a position i≥ 0  such that i+1 is the unique position  where  holds and
    _Γ()= (0)…(i)·^i+2.
   


By construction, it easily follows that  _Γ^((,)) is the set of well-formed traces in (_Γ,_Γ).
Then, the  formula θ_Γ captures the well-formed requirement and is defined as follows.


    [ ∧(→)∧(⋁_p∈Γ((p ↔ p)
    ∧∧)  ∨ ⋀_p∈Γ((p ↔ p)∧)  ∨;          (∧⋀_p∈Γ(p ↔ p) ∧⋁_p∈Γ (p ↔^2  p)  )) ]



This concludes the proof of Proposition <ref>.
 

