Davide Ciucci

Didier Dubois

From paraconsistent three-valued logics to multiple-source epistemic logic

Several interpretations can be given to the third truth value in three-valued logics. Here, we consider the case when it refers to the epistemic notion of contradictory, or both true and false at the same time. We study several paraconsistent threevalued logics that carry this concern and show that they can be translated into a fragment of a simple epistemic logic where modalities can only appear in front of literals. This logic is unusual in the sense that necessity modalities distribute over disjunctions instead of conjunctions. An equivalent translation into a fragment of KD modal logic can be obtained by exchanging the role of possibility and necessity modalities, highlighting the perfect symmetry between three-valued logics of contradiction and three-valued logics of incomplete information.

Introduction

The program of paraconsistent logics after Jaśkowski [START_REF] Jaśkowski | Propositional calculus for contradictory deductive systems[END_REF] is to find a logic which can manage contradictions and satisfies three requirements:

1. when applied to the contradictory systems would not always entail their over-completeness 1 ;

2. would be rich enough to enable practical inference;

would have an intuitive justification.

Nowadays, a consensual definition of what a paraconsistent logic is does not seem to exist, but a necessary condition is that the logical consequence relation is not explosive, that is, there can exist contradictions in the logic without implying that everything is true (point 1 above) -see introduction of [START_REF]Paraconsistency: Logic and applications[END_REF]. Several proposals to define such a logic have been studied in literature, following different lines: discursive logic, preservationism, adaptive logics, relevant logics, many valued logics [START_REF]Paraconsistency: Logic and applications[END_REF]. Here, we are interested in the case of many valued logics, most of which are based on a three-valued calculus.

In three-valued calculi, the intuition (point three above) which is attached to the third value is not always discussed and when it is, it often assumes an epistemic flavor, which can vary from unknown, contradictory to borderline [START_REF]Three-valued logics for incomplete information and epistemic logic[END_REF]. 1 A system is over-complete if any formula is a theorem.

Jaśkowski himself tried to use a third value to express paraconsistency, but he seems not to have a clear definition of what a contradiction stands for. He refers to theories with conflicting hypotheses, each one able to only partially explain the result of some experiment, or to facts that are not predictable a-priori. D'Ottaviano and Da Costa [START_REF] Ottaviano | Sur un problème de Jaśkowski[END_REF] cite, as a justification for their three-valued logic J 3 , the existence of contradictory theories in empirical disciplines for which we are (at the moment) not able to say which theory is the correct one, which sounds more like the idea of incomplete knowledge. In [START_REF] Asenjo | A calculus of antinomies[END_REF], the third value represents antinomies, that is, propositions that are at the same time true and false. The connectives used are Kleene ones and the same logic has been studied by Priest [START_REF] Priest | The Logic of Paradox[END_REF]. Although the meaning is not expressed clearly, it seems that the third value stands for both true and false, as in Belnap set-ups [START_REF] Belnap | A useful four-valued logic, Modern Uses of Multiple-Valued Logic[END_REF].

In the following, we try to provide a unified view of three-valued logics of paraconsistency, adopting this last interpretation of the third value: it represents the case of two sources (or two groups of sources) of information which assign a different (Boolean) truth value to a proposition (this is akin to the society semantics of Carnielli and Lima-Marques [START_REF] Carnielli | Society semantics for multiple-valued logics[END_REF]). We do it in the same style as we recently did for three-valued logics of incomplete information [START_REF]Three-valued logics for incomplete information and epistemic logic[END_REF], namely by translating many known three-valued paraconsistent formalisms into a very simple fragment of modal logic. This translation highlights the epistemic meaning of sentences in paraconsistent logics and facilitates a comparison among them.

A simple epistemic logic MELCC2 is introduced to deal with the interpretation of the third truth value in terms of conflict between sources. It is a two-layered logic: an objective level topped by an epistemic one, with no nested modal operators. In particular, it is different from the single-layer S5 discursive logic introduced by Jaśkowksi [START_REF] Jaśkowski | Propositional calculus for contradictory deductive systems[END_REF]. The paper lays bare the symmetry existing between threevalued paraconsistent logics and three-valued logics of incomplete information. It is shown that indeed MELCC possesses the properties of a KD modal logic provided that we exchange the possibility and necessity modalities.

Conflicting agents, three-valued logics and modal logic

Let us consider a set of propositional variables V = {a, b, c, . . . , p, . . . } and a standard propositional language L built on these symbols with the Boolean connectives of conjunction (∧), disjunction (∨), negation ( ′ ), and implication (→), plus tautology symbol (⊤). Suppose n logically sophisticated agents (i.e. they can use classical logic) sharing the same propositional language L, and capable to decide whether any proposition α ∈ L is true or false. In other words each agent possesses complete Boolean knowledge. Let Ω be the set of interpretations of L : {ω : V → {0, 1}}. It comes down to assuming that agent A i believes that the real world is w i ∈ Ω. For each formula α ∈ L, agent i can say whether it is true

(v i (α) = T i ) or false (v i (α) = F i ).
Let us consider a modal expression of the assertions made by the two agents. Let i α stand for the agent A i asserting the truth of α. Due to the complete knowledge assumption, each i is a trivial modality, i.e. i α ∨ i α ′ is true, so i and

♦ i coincide, since ♦ i α := ( i (α ′ )) ′ = i α.
In fact each modal system coincides with classical logic. Now, let us consider a three-valued logic L 3 . We denote by v(a) the truth value of the variable a, v(a) ∈ {0, 1, 1 2 }. We consider that these three values can be interpreted in the light of the joint assertions of both agent:

• v(a) = 1 means that all agents say that a is true

(v i (a) = T i , ∀i = 1, . . . , n); • v(a) = 0 means that all agents say that a is false (v i (a) = F i , ∀i = 1, . . . , n); • v(a) = 1
2 means that some agents say a is true, the other ones say a is false. This kind of setting was first introduced by Belnap [START_REF] Belnap | A useful four-valued logic, Modern Uses of Multiple-Valued Logic[END_REF] with agents having incomplete knowledge. It leads to a 4-valued truth-functional logic where the 4 values include unknown and contradictory. It also corresponds to the so-called society semantics [START_REF] Carnielli | Society semantics for multiple-valued logics[END_REF] where the authors (see also Dubois [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF]) indicate that only two agents are needed to render this meaning of truth-values without any loss of generality. This is what is assumed in the following. Thus, v(a) = 1 stands for the set {T 1 , T 2 }, v(a) = 0 stands for the set {F 1 , F 2 }, and the value of contradiction 1 2 stands for either set of truth values {T 1 , F 2 } or {T 2 , F 1 } 3 . This is pictured in Table 1. Now, let us define the collective modal symbols:

• p stands for "at least one source asserts p": p := 1 p ∨ 2 p. • If, as usual, we define ♦p := ( (p ′ )) ′ , we have that ♦p = ♦ 1 p ∧ ♦ 2 p = 1 p ∧ 2 p here (since 3 This convention is in accordance with Belnap logic where 1 2 is named BOTH and contrary to the approach in [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF] where contradiction is represented by the emptyset.

T 2 F 2 T 1 1 1 2 F 1 1 2 0
Table 1: Epistemic values from two complete sources each agent has complete knowledge), that is "both sources assert p".

We can then encode the assignment of L 3 truthvalues to a (Boolean) propositional variable a by means of the global modalities and ♦. To this end, on top of the standard propositional language L, we build another propositional language L which encapsulates L. It is another propositional language based on a set of variables V = { α : α ∈ L}, where the modality operator expresses necessity, as well as the classical connectives.

Let S ⊆ {0, 1, 1 2 } be a subset of L 3 truth-values. We denote by T (v(a) ∈ S) the modal translation of the set {v : v(a) ∈ S} corresponding to the statement v(a) ∈ S by an agent. Due to the proposed understanding of the three truth-values, the translation of the assignment of a subset of ternary truthvalues to an atom is a function T : 2 ({0,1, 1 2 } V ) → L from subsets of ternary valuations to the modal language L such that:

T (v(a) ≥ 1 2 ) = a T (v(a) ≤ 1 2 ) = a ′ T (v(a) = 1) = ♦a T (v(a) = 0) = ♦a ′ T (v(a) = 1 2 ) = a ∧ a ′ T (v(a) ∈ ∅) = ♦⊥ T (v(a) ∈ {0, 1}) = ♦a ∨ ♦b T (v(a) ≥ 0) = ⊤ So, 1
2 means that one source asserts a and the other a ′ . Moreover, since in paraconsistent logics designated values are usually 1 2 and 1, we see that a corresponds to asserting a in a paraconsistent logic. Note that this is NOT a syntactic translation from one logic to another: it provides a tool for expressing the semantics of one logic into the syntax of another one.

The target modal system

We denote by α, β, . . . the propositional formulae of L, and φ, ψ, . . . the modal formulae of V . A logic that uses the language L defined above, called MELC [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF] has been proposed as a minimal epistemic logic with conflicts. It uses the propositional logic axioms, and some modal ones:

1. φ → (ψ → φ) 2. (ψ → (φ → µ)) → ((ψ → φ) → (ψ → µ)) 3. (φ ′ → ψ ′ ) → (ψ → φ) (RE) α ≡ β if and only if ⊢ α ≡ β (RM) α → β if ⊢ α → β in PL (3-C) α ∧ β ∧ γ → (α ∧ β) ∨ (α ∧ γ) ∨ (β ∧ γ) (N) ⊤; (POS) ♦⊤
The only rule is modus ponens: If ψ and ψ → φ then φ. This is a fragment of the non-regular logic EMN [START_REF] Chellas | Modal logic: an introduction[END_REF] (except for axiom 3-C). Semantics are usually expressed in terms of neighborhood semantics, but they can be related to the multisource environment suggested above. Concerning semantics, denote the set of classical models of α by [α] = {ω : ω |= α}. Each source has its own epistemic state

E i ⊆ Ω. A (meta)-interpretation of L is a pair (E 1 , E 2 ), with E 1 , E 2 = ∅.
We define satisfiability as:

• (E 1 , E 2 ) |= α if E 1 ⊆ [α] or E 2 ⊆ [α]; • (E 1 , E 2 ) |= φ ∧ ψ if (E 1 , E 2 ) |= φ and (E 1 , E 2 ) |= ψ; • (E 1 , E 2 ) |= φ ′ if (E 1 , E 2 ) |= φ is false.
In this setting, axiom (3-C) expresses the fact that there are exactly two sources.

α can be expressed as the disjunction 1 α ∨ 2 α corresponding to KD modalities [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF]. Semantic inference of a formula from a modal base B is defined in the usual way:

B |= φ if and only if ∀E 1 , E 2 = ∅ ⊆ Ω, if (E 1 , E 2 ) |= ψ, ∀ψ ∈ B, then (E 1 , E 2 ) |= φ.
The logic we want to consider here is an extension of MELC that takes into account the fact that we can have contradictions and that the knowledge of each agent is complete. As a consequence, the modalities constructed in the previous section have distinguished properties. Due to the fact that both sources are complete, there is the following (unusual) property, for general Boolean propositions.

Proposition 3.1. For any proposition, α ∨ β is equivalent to (α ∨ β).
Proof. This is easily derived from the definition of and the fact that we suppose the knowledge complete, that is for each agent A i it holds for i . However, we do not have that α ∧ β is equivalent to (α ∧ β). Likewise, the following property holds : α∨ α ′ is a tautology. From it, we can also derive ♦α → α, which represents the idea that ♦ stands for an agreement of the two sources, both asserting that α is true, whereas just expresses the idea that one of the two is true, but not necessarily both. Finally the MELCC system is MELC plus deviant modal axioms:

(N ∨) ⊢ (α ∨ β) → ( α ∨ β); (D t ) ⊢ ♦α → α.
The semantics of this system is the same as MELC, except that now, (E 1 , E 2 ) = ({w 1 }, {w 2 }) in the above definitions of satisfiability and semantic inference. This is enforced by axiom (N ∨). Moreover, (N ) becomes a redundant axiom. At this point, we are equipped with sufficient tools to make sense of three-valued paraconsistent logics inside the multisource epistemic logic MELCC, via a translation of their connectives and axioms. We start with the simplest one, that is Priest logic.

Translation of Priest logic

Priest [START_REF] Priest | The Logic of Paradox[END_REF] attaches to the third truth value the meaning of a paradox; it refers to sentences that are "both true and false" His intention is to "isolate paradoxes and prevent them from contaminating everything else".

To define the basic connectives, his reasoning implicitly assumes that a sentence can have the following values {0}, {0, 1}, {1} and then he extends the classical Boolean truth tables to set-valued arguments (see also [START_REF] Lawry | A bipolar model of assertability and belief[END_REF][START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF]). So if A is true and B paradoxical, he gets {1}∧{0, 1} = {1∧0, 1∧1} = {0, 1}, i.e. paradoxical. Hence, Kleene strong truth tables are recovered, that is the minimum ⊓, the maximum ⊔, and the involutive negation ¬, the material implication a → P b := ¬a ⊔ b of a Kleene lattice. However, in his system both 1 and 1 2 are designated. In fact, the notion of semantic inference is defined as follows: Definition 1. If B is a set of propositions in Kleene logic, then B P α if and only if there does not exist an interpretation v such that v(α) = 0 and for all

β ∈ B, v(β) ∈ {1, 1 2 }. In other words, if v(β) ≥ 1 2 , ∀β ∈ B then v(α) ≥ 1 2 .
As a result, all Boolean tautologies are still valid, but modus ponens does not hold any longer. A similar intuition of the third value is given by Asenjo [START_REF] Asenjo | A calculus of antinomies[END_REF] to deal with antinomies and he also comes up with Kleene truth tables.

If the knowledge base B in Priest logic contains an atom a, it means that v(a) ≥ 1 2 , that is, we write a in MELCC. If B contains the conjunction of two atoms a ⊓ b, this is translated as:

T (v(a ⊓ b) ≥ 1 2 ) = a
T (v(α ⊓ β) ≥ i) = T (v(α) ≥ i) ∧ T (v(β) ≥ i), i ≥ 1 2 T (v(α ⊔ β) ≥ i) = T (v(α) ≥ i) ∨ T (v(β) ≥ i), i ≥ 1 2 T (v(¬α) ≥ 1 2 ) = T (v(α) ≤ 1 2 ) Note that T (v(¬α) ≥ 1 2 ) = (T (v(α) = 1)) ′ .
Implication statements can be translated by means of other connectives or directly:

T (v(α → P β) ≥ 1 2 ) = T (v(α) = 1) → T (v(β) ≥ 1 2
). Applied to atoms a and b, implication statement a → P b ∈ B translates into:

T (v(a → P b) ≥ 1 2 ) = ♦a → b = a ′ ∨ b.
Note that in contrast T (v(α

→ P β) = 1) = T (v(α) ≥ 1 2 ) → T (v(β) = 1), so that T (v(a → P b) = 1) = a → ♦b = ♦a ′ ∨ ♦b.
Note that all subsets of ({0, 1, 1 2 } V ) can be expressed as {v : v(α ∈ S)} for some subset S of truth-values and some Priest logic formula α. So, by extending function T to all formulas built with connectives of Priest logic, we make it a mapping.

Let α be a formula in conjunctive normal form (without simplifying the terms of the form a ⊓ ¬a). Now, since designated truth values are 1 and 1 2 , its translation into MELCC consists in the same classical conjunction of disjunctions where we put a modality in front of all literals. So, if we replace all literals l by l, any propositional tautology in this form remains a tautology in MELCC. Clearly, the fragment of MELCC we can capture is just given by the conjunction and disjunction of literals preceded by a . That is: a| a ′ |ψ ∨ φ|ψ ∧ φ. In Priest logic, we do not have modus ponens. This is captured in MELCC, noticing that from a and ♦a → b it does not follow b. Similarly, α⊓¬α ⊢ β does not hold, and this is expressed by the fact that a ∧ a ′ is not a contradiction in MELCC. Given a formula α in Priest logic and a model for its translation into MELCC, we are now able to define a three-valued interpretation for α. 2 ) the interpretation v (w1,w2) defined below is a model of α: ∀a,

v (w1,w2) (a) =                1 (w 1 , w 2 ) ♦a (that is, w 1 |= a and w 2 |= a) 0 (w 1 , w 2 ) ♦¬a (that is, w 1 |= a and w 2 |= a) 1 2
otherwise

The other way around does not hold, strictly speaking. Indeed, given a pair (w 1 , w 2 ) of Boolean evaluations, we are able to define the corresponding three-valued valuations. On the contrary, if we have a three-valued valuation, we are not able to distinguish between the two sources that generated it. However, this is not a real issue : in MELCC, the two models (w 1 , w 2 ) and (w 2 , w 1 ) satisfy the same set of formulas and are indeed indistinguishable; in fact MELCC models are to be viewed, like two-element models of MEL, as doubletons of interpretations (i.e. sets, not pairs). In fact, another translation is possible into MEL [START_REF]Three-valued logics for incomplete information and epistemic logic[END_REF]. It is exactly like the above translation, exchanging and ♦. The two translations are then isomorphic.

Translation of A and J 3 logics

This is the logic proposed by Asenjo and Tamburino in [START_REF] Asenjo | Logic of antinomies[END_REF]. Connectives are min, max, involutive nega-tion and Jaskowksi implication4 : the designated

→ J 0 1 2 1 0 1 1 1 1 2 0 1 2 1 1 0 1 2 1 Table 2: Jaśkowski implication
values are 1 and 1 2 . The only difference with respect to Priest is the introduction of the new implication → J , whose translation into MELCC is as follows.

T (v(α → J β) = 1) = T (v(α) ≥ 1 2 ) → T (v(β) = 1) T (v(α → J β) ≥ 1 2 ) = T (v(α) ≥ 1 2 ) → T (v(β) ≥ 1 2 )
If α = a, β = b are atoms, we obtain respectively a → ♦b and a → b. Clearly, in this logic modus ponens does hold. Indeed, it corresponds in MELCC to state that from T (v(α) ≥

2 ) → T (v(β) = 1) and T (v(α) ≥ 1 2 ), it follows T (v(β) = 1). On the other hand, not all classical tautologies are valid. But if we consider the fragment of A without ¬ we have that all classical tautologies are still valid in A (this has also been stated in [START_REF] Ottaviano | Sur un problème de Jaśkowski[END_REF] for the equivalent logic J 3 , see below).

We note that the negation ∼α := α → J 0 is an intuitionistic one and we have the equality α → J β = ∼α ∨ β. At the atomic level, the translation into MELCC of the negation ∼a is T (v(∼a) = 1) = T (v(∼a) ≥ 1 2 ) = (♦a) ′ = a ′ . So the fragment in MELCC which corresponds to the A logic is a| a ′ |φ ′ |φ∧ψ|φ∨ψ, that is the language of MELCC where modalities are in front of literals only. Proposition 4.1 can be extended to Jaśkowski implication.

In [START_REF] Ottaviano | Sur un problème de Jaśkowski[END_REF] the authors introduce the logic J 3 to answer points 1-3 of Jaśkowski. The primitive connectives are max, the involutive negation and the unary strengthening operator ∇ such that ∇0 = 0, ∇ 1 2 = ∇1 = 1. Among the derived operations, it is worth to mention Jaśkowski implication as a → J b := ¬∇a ∨ b and Łukasiewicz implication as a → L b := (∇¬a ∨ b) ∧ (∇b ∨ ¬a). If we explicitly express ∇ in MELCC we have that for a given atom a, ∇a is translated into a. Further, it can be easily seen that ∇ is also definable in A as ∇a = ¬(a → J 0), so A and J 3 have the same connectives and all the results proved for A also hold for J 3 .

Finally, in [START_REF] Asenjo | Logic of antinomies[END_REF] an axiomatic system is proposed for the logic A, that takes into account the distinction between antinomic vs. non-antinomic statements, distinction at the basis of the logic A. This difference looks hardly expressible in MELCC, in particular the axiom asserting B i ⊓¬B i with B i an atomic antinomy (that is both B i and ¬B i are provable).

Translation of RM3 (Sobociński) logic

The same connectives that define A, also define the relevance logic RM →J 3 [START_REF] Avron | On An Implication Connective of RM[END_REF] (→ J is denoted by ⊃ in the original paper), which is also equivalent to RM3 [START_REF] Anderson | The logic of relevance and necessity[END_REF][START_REF] Brady | Completeness proofs for the systems RM3 and BN4[END_REF], that is to Sobociński [START_REF] Sobociński | Axiomatization of a partial system of three-value calculus of propositions[END_REF][START_REF] Avron | On An Implication Connective of RM[END_REF] logic through the following mutual definitions: p → S q := (p → J q) ∧ (¬q → J ¬p) p → J q := q ∨ (p → S q) Thus, even if Sobociński and RM3 were not conceived to deal with paraconsistency, they can play a role in this framework: in [START_REF] Avron | On An Implication Connective of RM[END_REF], it is claimed that RM →J 3 "might be considered an optimal paraconsistent logic".

As a consequence of all these equivalences, all above translation results also apply to RM3 and Sobociński logic. In particular, Sobociński implication whose truth table is on Table 3 can be translated as

T (v(α → S β) = 1) = [T (v(α) ≥ 1 2 ) → T (v(β) = 1)] T (v(α → S β) ≥ 1 2 ) = [T (v(α) ≥ 1 2 ) → T (v(β) ≥ 1 2 )] ∧ [T (v(α) = 1) → T (v(β) = 1)] → S 0 1 2 1 0 1 1 1 1 2 0 1 2 1 1 0 0 1 ∧ S 0 1 2 1 0 0 0 0 1 2 0 1 2 1 1 0 1 1 ∨ S 0 1 2 1 0 0 0 1 1 2 0 1 2 1 1 1 1 1

Table 3: Sobociński implication, conjunction and disjunction

For atoms, it respectively yields a → ♦b and

( a → b) ∧ (♦a → ♦b).
Sobociński conjunction and disjunction can be translated into MEL from Table 3 or by means of the definition α∧ S β = ¬(α → S ¬β) and de Morgan properties.

On atoms they read as

T (v(a ∧ S b) = 1) = ( a ∧ ♦b) ∨ (♦a ∧ b) T (v(a ∧ S b) ≥ 1 2 ) = a ∧ b T (v(a ∨ S b) = 1) = ♦a ∨ ♦b T (v(a ∨ S b) ≥ 1 2 ) = ♦a ∨ ♦b ∨ ( a ∧ a ′ ∧ b ∧ b ′ )
As far as the axiom system is concerned and due to the equivalence between the RM3 and Sobociński logics, we just consider the axiom system of RM3 [START_REF] Brady | Completeness proofs for the systems RM3 and BN4[END_REF].

(R1) α → S α; (R2) (α ⊓ (α → S β)) → S β; (R3) α ⊓ β → S α; (R4) α ⊓ β → S β; (R5) ((α → S β) ⊓ (α → S γ)) → S (α → S (β ⊓ γ)); (R6) (α → S ¬α) → S ¬α; (R7) (α → S ¬β) → (β → S ¬α); (R8) (¬¬α → S α); (R9) (¬α ⊓ β) → (α → β); (R10) ¬α → S (α ⊔ (α → β)); Inference rules are: 1. α and α → S β implies β 2. α and β implies α ⊓ β 3. α → S β and γ → S δ implies (β → S γ) → S (α → S δ) Lemma 1. If α is a formula in RM3 logic, then T (v(α) ≥ 1 2 ) ∨ T (v(α) ≤ 1 2 ) is a tautology in MELCC.
Proof. The proof (omitted here) is by induction on the structure of α.

Proposition 6.1. If A is an axiom in RM3 logic, then T (v(A) ≥ 1
2 ) is a tautology in MELCC. Proof. Axioms (R1), (R3), (R4) and (R8) are easily proved. Axiom (R2). It is the conjunction of two tautologies. The first one follows from the fact that (R2) holds in Boolean logic and the second one by Lemma 1. Axiom (R5) and (R7) are the conjunctions of two tautologies that easily follows by the fact that (R5) is a Boolean theorem. Axiom (R6) is the conjunction of two tautologies. The first one is just lemma 1 and the second one the Boolean version of axiom (R6). Axiom (R9) is the conjunction of two tautologies. The second one is just axiom R9 in Boolean logic. The first half is:

(T (v(¬α) ≥ 1 2 )∧T (v(β) ≥ 1 2 )) → [(T (v(α) ≥ 1 2 ) → T (v(β) ≥ 1 2 )) ∧ (T (v(α) = 1) → T (v(β) = 1)], that is: T (v(α) = 1) ∨ (T (v(β) ≥ 1 2 )) ′ ∨ [(T (v(α) ≥ 1 2 ) ′ ∨ T (v(β) ≥ 1 2 )) ∧ (T (v(α) = 1) ′ ∨ T (v(β) = 1)].
Then by distributivity, we can simplify as

T (v(α) = 1) ∨ (T (v(β) ≥ 1 2 )) ′ ∨ (T (v(α) = 1) ′ ∨ T (v(β) = 1),
which is a Boolean tautology. Axiom [START_REF]Three-valued logics for incomplete information and epistemic logic[END_REF] is translated into the following two tautologies:

T (v(α) = 1) ∨ (T (v(α) ≥ 1 2 ) ∨ [((T (v(α) ≥ 1 2 ) ′ ∨ T (v(β ≥ 1 2 )) ∧ (T (v(α) = 1) ′ ∨ T (v(β) = 1))] and T (v(α) ≥ 1 2 ) ∨ T (v(α) = 1) ∨ (T (v(α) ≥ 1 2 ) ′ ∨ T (v(β) = 1).
Inference rules can be checked to hold in the translation into MELCC.

Translation of Sette logic

Sette [START_REF] Sette | On propositional calculus P_1[END_REF] introduced a paraconsistent logic with the aim to give a logic for "inconsistent (but not absolutely inconsistent) formal systems". Its connectives are on Table 4. In this logic, the intuitionistic nega-

→ Se 0 1 2 1 0 1 1 1 1 2 0 1 1 1 0 1 1 x -x 0 1 1 2 1 1 0 ∧ Se 0 1 2 1 0 0 0 0 1 2 0 1 1 1 0 1 1 ∨ Se 0 1 2 1 0 0 1 1 1 2 1 1 1 1 1 1 1
Table 4: Sette logic connectives tion is definable as ∼ a := a → Se 0. The peculiarity of this logic is that conjunction and disjunction can be expressed from implication and negation as follows (they are not min and max):

x ∧ Se y := (((x → Se x) → Se x) → Se -((y → Se y) → Se y)) → Se -(x → Se -y) x ∨ Se y := (x → Se --x) → Se (-x → Se y)
The meaning of the third value is not discussed, but the connectives (see Table 4), except for negation, suggest no difference between 1 and 1 2 . The lation of Sette connectives in MELCC is thus the same in the two cases ≥ 1 2 and = 1:

T (v(α → Se β) ≥ 1 2 ) = T (v(α ≥ 1 2 ) → T (v(β ≥ 1 2 ) T (v(α ∧ Se β) ≥ 1 2 ) = T (v(α ≥ 1 2 ) ∧ T (v(β ≥ 1 2 ) T (v(α ∨ Se β) ≥ 1 2 ) = T (v(α ≥ 1 2 ) ∨ T (v(β ≥ 1 2 )
For atoms we have

T (v(-a) ≥ 1 2 ) = a ′ and T (v(a → Se b) ≥ 1 2 ) = a → b; T (v(a ∧ Se b) ≥ 1 2 ) = a ∧ b; T (v(a ∨ Se b) ≥ 1 2 ) = a ∨ b.
Note that this is the same translation as conjunctions and disjunctions of Priest logic (the min and the max) and Jaśkowksi implication.

An axiom system together with modus ponens is given such that the logic (named P 1 ) is complete and "cannot be strengthened (i.e., there is no propositional calculus between P 1 and P 0 , where P 0 is the classical propositional calculus)". In other words, if we add to P 1 any tautology which holds in P 0 but not in P 1 we get P 0 . The axioms are:

(S1) α → Se (β → Se α) (S2) (α → Se (β → Se γ)) → Se ((α → Se β) → Se (α → Se γ)) (S3) (-α → Se -β) → Se ((-α → Se --β) → Se α) (S4) -(α → Se --α) → Se α (S5) (α → Se β) → Se --(α → Se β)
and the rule of inference is modus ponens. We note that modus ponens holds also in the translation. Indeed, since we consider both 1 and 1 2 as designated values, it corresponds to: "from

T (v(α) ≥ 1 2 ) and T (v(α) ≥ 1 2 ) → T (v(β) ≥ 1 2 ) it follows T (v(β) ≥ 1 2 )", which clearly holds in MELCC. Proposition 7.1. If A is an axiom in Sette logic, then T (v(A) ≥ 1
2 ) is a tautology in MELCC. Proof. Lemma 1 applies to Sette Logic. Axioms (S1) and (S2) are Boolean axioms, thus they easily follow. For axiom (S3), we use recursive translation rules and come down to a formula of the form

T (v(α) ≤ 1 2 )∨T (v(α) ≥ 1 2 )
, which is a tautology by lemma 1. Axioms (S4, S5) are proved in a similar manner.

The fragment of MELCC capturing Sette logic is thus: a| a ′ |ψ ′ |ψ ∧ φ|ψ ∨ φ, the same as for J 3 and Sobociński's logics.

Sette logic connectives are definable in Łukasiewicz three-valued logic as follows [START_REF] Da | Relations between paraconsistent logics and many-valued logic[END_REF]:

α ∧ Se β := ¬(α ∧ β) → L (α ∧ β) and α → Se β := J 0 (β) → L J 0 (α)
, where J 0 (α) := ¬α ∧ Se ¬(α ∧ Se ¬α) and ∧ denotes the minimum; J 0 returns 1 if and only if α = 0. The converse does not hold since with Sette connectives is not possible to obtain the value 1 2 . So, even if the three 3-valued logics J 3 , RM 3 and Sette are not equivalent, they share the same paraconsistent behaviour: they can be expressed in the same MELCC fragment where the only language restriction is the presence of modalities only in front of literals, and conjunction, disjunction and implication have the same translation.

The symmetry between paraconsistent and incomplete information logics

Note that Proposition 1 says that the necessity modality behaves like a possibility modality ♦ in the sense of usual regular modal logics. Namely, exchanging the notation and ♦, the modal axioms of MELCC become

1. φ → (ψ → φ) 2. (ψ → (φ → µ)) → ((ψ → φ) → (ψ → µ)) 3. (φ ′ → ψ ′ ) → (ψ → φ) (RE) α ≡ β if and only if ⊢ α ≡ β (RM) ♦α → ♦β if ⊢ α → β in PL (3-D) ♦α ∧ ♦β ∧ ♦γ → ♦(α ∧ β) ∨ ♦(α ∧ γ) ∨ ♦(β ∧ γ) (N) ⊤; (POS) ♦⊤ (Π∨) ♦(α ∨ β) → (♦α ∨ ♦β) (D) α → ♦α
Unsurprisingly, these axioms (but for (3-D)) are typical of the KD systems, and (POS) is redundant, this time. These axioms actually characterize the fragment of KD, called MEL (Meta-or Minimal Epistemic Logic) [START_REF] Banerjee | A simple modal logic for reasoning about revealed beliefs[END_REF]. In fact, the syntax of MELCC is exactly the same as the one of MEL. The MEL system (with Modus Ponens rule) has been proved sound and complete with respect to the following satisfiability relation, where epistemic states (nonempty sets E ⊆ Ω) and semantic inference of a formula from a modal base B:

• E |= α if E ⊆ [α]; • E |= φ ∧ ψ if E |= φ and E |= ψ; • E |= φ ′ if E |= φ is false. • B |= φ if and only if ∀E ⊆ Ω, if E |= ψ, ∀ψ ∈ B, E |= φ.
MEL is also a syntactic rendering of Boolean possibility theory. Namely, an epistemic state E induces two Boolean set functions N and Π on 2 Ω defined by N (A) = 1 if E ⊆ A and 0 otherwise (this is the necessity measure expressing the modality here) and Π(A) = 1 if E ∩ A = ∅ and 0 otherwise (this is the possibility measure expressing the ♦ modality)

We thus consider a fragment of MELC [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF], which has been conceived for two possible incomplete contradictory sources, and strengthen it in order to capture completeness of information. It is easy to check that axiom (3-D) induced from (3-C) enforces epistemic states satisfying the MEL axioms to contain only one or two classical interpretations, i.e., be of the form E = {w 1 , w 2 }. Indeed if E = {w 1 , w 2 , w 3 } then we may have

w 1 ∈ A ∩ B c ∩ C c , w 2 ∈ A c ∩ B ∩ C c , w 3 ∈ A c ∩ B c ∩ C, so that Π(A) = Π(B) = Π(C) = 1 but Π(A ∩ B) = Π(A ∩ C) = Π(B ∩ C) = 0.
However, with only two elements

w 1 , w 2 , Π(A) = Π(B) = Π(C) = 1 implies that at least one of Π(A∩ B), Π(A ∩ C), Π(B ∩ C), is 1. Indeed we cannot choose w 1 ∈ A ∩ B c ∩ C c , w 2 ∈ A c ∩ B ∩ C c , since Π(C) = 1, which enforces either Π(A ∩ C) = 1 or Π(B ∩ C) = 1.
The total symmetry between systems MELCC and MEL+(3-D) can thus be viewed at the semantic level in terms of possibility theory :

α holds in MELCC if and only if w 1 ∈ [α] or w 2 ∈ [α], if and only if {w 1 , w 2 } ∩ [α] = ∅ if and only if ♦α holds in MEL+(3-D).
Interestingly the MEL system is the target language for the translation of three-valued logics of incomplete information where the third truth-value means unknown (such as Kleene logic) [START_REF]Three-valued logics for incomplete information and epistemic logic[END_REF]. We denote by T M EL (v(a) ∈ T ) the translation into MEL of the statement v(a) ∈ T , with the same understanding as in Section 3:

T M EL (v(a) = 1) = a T M EL (v(a) = 0) = a ′ T M EL (v(a) = 1 2 ) = ♦a ∧ ♦a ′ T M EL (v(a) ≥ 1 2 ) = ♦a T M EL (v(a) ≤ 1 2 ) = ♦a ′
which can be compared with the translation into MELCC : and ♦ are again exchanged. Note that the fragment of MEL obtained from translating truth-assigned formulae in three-valued logics only uses modal atoms of the form ℓ, where ℓ is a literal [START_REF]Three-valued logics for incomplete information and epistemic logic[END_REF]. As a consequence, this fragment does not contain axiom 3-D, since the latter puts ♦ in front of conjunctions of atoms, and cannot be expressed in terms of a propositional formula with atoms ℓ. So the presence of axiom 3-D is immaterial for the translation from three-valued logics to MEL. The same remark can be done for MELCC with respect to axiom 2-C. This is reflected by the fact that even if the number of agents can be restricted to two, this number is immaterial in the definitions of the three truth-values.

In summary, it is immaterial to choose the translation T into MELCC or translation T M EL into MEL. In other words, T M EL (v(a) ≥ 1

2 ) in MEL behaves just as T (v(a) ≥ 1 2 ) in MELCC in the sense that we can map sentences in a MELCC base into sentences in a MEL base by swapping ♦ and , while preserving the same deductive closures (up to the renaming of modalities). More precisely, if K a set of sentences in L , denote by σ(K) the set of sentences obtained by swapping the two modalities and ♦. If B = {α i : i = 1, . . . n} is a set of sentences in one of the paraconsistent logics mentioned above and C denotes the deductive closure, we have that:

C M EL (T M EL (B)) = σ(C M ELCC (T (B))),
where T (B) = {T (α i ) : i = 1, . . . n}. So both MELCC and MEL +(3-D) can be used as the target language for three-valued paraconsistent logics. For instance, the fact that Sette logic is reputed to be a maximal logic less than propositional logic is retrospectively not mysterious, and can be seen in the modal translation at the semantic level. One can claim that MEL + (3-D) is really an epistemic logic expressing knowledge as little incomplete as possible, since epistemic states that serve as models contain not more than two interpretations. Enforcing an additional constraint will reduce such epistemic states to standard interpretations and leads a collapse into propositional logic.

Note that the Belnap [START_REF] Belnap | A useful four-valued logic, Modern Uses of Multiple-Valued Logic[END_REF] truth-values unknown and contradictory, indeed play symmetric roles in the bilattice structure (the two three-valued logics obtained by deleting one of these values coincide with a Kleene structure).

Conclusion

This paper suggests that the two-completelyinformed-agent modal logic MELCC is a natural framework for reasoning under contradictory information in the style of several existing three-valued paraconsistent logics, when the third truth value means both true and false. The restriction to the fragment of MELCC putting modalities only in front of literals is the price paid by the truthfunctionality of these logics. MELCC thus offers an encompassing framework, where it is possible to express the fact that a conjunction is not paraconsistent while each of its conjoints is (typically the case where w 1 |= a ∧ b ′ and w 2 |= a ′ ∧ b).

As MELCC may look like a baroque modal system (since the roles of the usual modalities are exchanged), it is important to point out that the modal framework for the translation is equivalently the one of MEL [START_REF] Banerjee | A simple modal logic for reasoning about revealed beliefs[END_REF], that is, logic KD without modality nesting and purely modal formulas, provided that and ♦ are swapped in the translation. It highlights the fact that three-valued paraconsistent logics are symmetric to logics of incomplete information (for instance Priest and Kleene logics can be paired). So, the choice of the meaning of the third truth-value (unknown vs. contradictory) does not affect the translation into MEL, but for the choice between (if 1/2 = unknown) and ♦ (if 1/2 =contradictory) when prefixing the translations of atoms of the concerned three-valued language. It seems that given a 3-valued logic, the choice between the two meanings of the third truth-value (unknown and contradictory) is a matter of choosing the designated truth values (1 for unknown and 1, 1 2 for contradictory); it remains to be understood what makes one system of paraconsistent logic more attractive than another one, and what the translations into modal logic, where the meaning of implications is clear, can contribute to this issue.

Clearly, we can deal with both flaws in information, incomplete and contradictory knowledge, together. In this case, we need four values, in the style of Dunn-Belnap logic, and the next step is to formally show that the logic MELC introduced in [START_REF] Dubois | Reasoning about ignorance and contradiction: many-valued logics versus epistemic logic[END_REF] plays for Belnap logic the same role as MEL plays for Kleene logic and MELCC for Priest logic.

  ∧ b and similarly for the disjunction. Note that T (v(a⊓ b) = 1) = ♦a∧♦b. Translations of formulae declared as true in Priest Logic are defined recursively.

Proposition 4 . 1 .

 41 Let α be a formula in Priest logic. For any model (w 1 , w 2 ) of T (v(α) ≥ 1

It stands for Minimal Epistemic Logic with Completeness and Conflict

Note that Jaśkowski traces back this implication to Słupecki

Acknowledgment

The authors wish to thank Philippe Besnard for remarks on the first draft that led us to improve the presentation.


Philippe Balbiani

Emiliano Lorini

Ockhamist Propositional Dynamic Logic: A Natural Link between PDL and CTL *

We present a new logic called Ockhamist Propositional Dynamic Logic, OPDL, which provides a natural link between PDL and CTL * . We show that both PDL and CTL * can be polynomially embedded into OPDL in a rather simple and direct way. More generally, the semantics on which OPDL is based provides a unifying framework for making the dynamic logic family and the temporal logic family converge in a single logical framework. Decidability of the satisfiability problem for OPDL is studied in the paper.

Introduction

Different logical systems are traditionally used in theoretical computer science and in artificial intelligence for the verification of programs and for modelling reactive systems and multi-agent systems. Among them we should mention Propositional Dynamic Logic PDL [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF], Propositional Linear Temporal Logic PLTL [START_REF] Pnueli | The temporal logic of programs[END_REF], Computation Tree Logic CTL [START_REF] Emerson | Temporal and modal logic[END_REF], Full Computation Tree Logic CTL * [START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF] and Alternating-time Temporal Logic ATL [START_REF] Alur | Alternating-time temporal logic[END_REF]. Some relationships between these different logical systems have been studied. For instance, it is well-known that PLTL and CTL are fragments of CTL * and that CTL is a fragment of ATL [START_REF] Goranko | Coalition games and alternating temporal logics[END_REF]. However, at the current stage, the general picture remains incomplete. For example, it is clear (and well-known) that the logic of programs PDL can express properties that Full Computation Tree Logic CTL * cannot and vice-versa. Moreover, there are no clear relationships between PDL and logics of strategic reasoning such as ATL. More precisely, it is not known whether there exists natural embeddings of PDL into ATL or of ATL in PDL. Even more importantly, there is still no logical system that can be said to be more general than the others. For instance, there is no logic that embeds in a natural and simple way both PDL and CTL * . Indeed, although there exist some logics that embed both PDL and CTL * , they do it in a rather complicated and unnatural way. For example, it is well-known that PDL and CTL * can be embedded in modal µ-calculus. However, although the embedding of PDL into modal µ-calculus is simple and direct, the embedding of CTL * into modal µcalculus is rather complicated and doubly exponential in the length of the input formula [START_REF] Dam | CTL* and ECTL* as fragments of the modal mu-calculus[END_REF]. Another logic that links PDL with CTL * is the extension of PDL with a repetition construct (PDL-∆) by [START_REF] Streett | Propositional dynamic logic of looping and converse is elementarily decidable[END_REF]. But again, the embedding of CTL * into PDL-∆ too is rather complicated and doubly exponential in the length of the input formula [START_REF] Wolper | A translation from full branching time temporal logic to one letter propositional dynamic logic with looping[END_REF]. 1For this reason, a challenge arises of making the previous competing logical systems converge into a single logical system. The aim of this paper is to make a step into this direction by proposing an Ockhamist variant of Propositional Dynamic Logic, OPDL, that provides a natural link between PDL and CTL * . Specifically, we show that both PDL and CTL * can be polynomially embedded into OPDL in a rather simple and direct way. More generally, the Ockhamist semantics on which OPDL is based provides a unifying framework for making the dynamic logic family and the temporal logic family converge into a single logical framework. Ockhamist semantics for temporal logic have been widely studied in the 80ies and in the 90ies [START_REF] Thomason | Combinations of tense and modality[END_REF][START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF][START_REF] Brown | An extended branching-time ockhamist temporal logic[END_REF]. The logic of agency STIT (the logic of "seeing to it that") by Belnap et al. [START_REF] Belnap | Facing the future: agents and choices in our indeterminist world[END_REF] is based on such semantics. According to the Ockhamist conception of time (also called indeterminist actualist, see [START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF]) the truth of statements is evaluated with respect to a moment and to a particular actual linear history passing through that moment, and the temporal operators are relativized to the actual history of the evaluation.

The rest of the paper is organized as follows. We first present the syntax and the semantics of OPDL and provide a decidability result for this logic (Section 2). Then, we discuss, in Section 3, about the relationship of OPDL with PDL and CTL * (Section 3). In particular, we provide polynomial reductions of PDL and CTL * to OPDL. In Section 4 we present a variant of OPDL whose semantics is based on the notion of labeled transition system (LTS). In Section 5 we conclude by discussing some perspectives for future work. 2

Ockhamist Propositional Dynamic Logic

The distinction between the 'Ockhamist' semantics and the 'Peircean' semantics for branching-time temporal logic was proposed by Prior in his seminal work on the logic of time [START_REF] Prior | Past, Present, and Future[END_REF] (see also [START_REF] Thomason | Combinations of tense and modality[END_REF]). According to the 'Peircean' view the truth of a temporal formula should be evaluated with respect either to some history or all histories starting in a given state. In the 'Ockhamist' semantics for branching time a notion of actual course of events is given. In particular, according to the 'Ockhamist' view, the truth of a temporal formula should be evaluated with respect to a particular actual history starting in a given state. While the branching-time temporal logic CTL * is compatible with the Ockhamist conception of time, the semantics for PDL in terms of labelled transition systems is closer to the Peircean view than to the Ockhamist view since it does not consider a notion of actual history or actual path in a transition system. The logic OPDL can be conceived as a variant of the logic of programs PDL based on the Ockhamist view of time. Specifically, OPDL is a variant of PDL in which the truth of a formula is evaluated with respect to a given actual history. The syntax and the semantics of this logic are presented in Sections 2.1 and 2.2.

Syntax

Assume a countable set Prop of atomic propositions (with typical members denoted p, q, . . .) and a countable set Atm of atomic programs (or atomic actions) (with typical members denoted a, b, . . .). Let 2 Atm * = 2 Atm \{∅}. The language L OPDL (Prop, Atm) of OPDL consists of a set Prg of programs and a set Fml of formulae. It is defined as follows:

Prg : π ::= a |≡| (π 1 ; π 2 ) | (π 1 ∪ π 2 ) | π * | ϕ? Fml : ϕ ::= p | ¬ϕ | (ϕ 1 ∧ ϕ 2 ) | [[π]]ϕ
where p ranges over Prop and a ranges over Atm. We adopt the standard definitions for the remaining Boolean operations. The dual π of the operator [[π]] is defined in the expected way: π ϕ def = ¬[[π]]¬ϕ. We follow the usual rules for omission of the parentheses. Given a formula ϕ, let F L(ϕ) denote its Fischer-Ladner closure. See [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]Chapter 6] for details. It is a well-known fact that card(F L(ϕ)) is linear in the length of ϕ.

Complex programs of sequential composition (π 1 ; π 2 ), non-deterministic choice (π 1 ∪ π 2 ), iteration (π * ) and test (ϕ?) are built from atomic programs in Atm, from the special program ≡ and from formulae in Fml . The special program ≡ allows to move from a history to an alternative history passing through the same moment. The behavior of this program will become clearer in Section 2.2 when presenting the OPDL semantics.

The formula [[π]]ϕ has to be read "ϕ will be true at the end of all possible executions of program π" whereas π ϕ has to be read "ϕ will be true at the end of some possible execution of program π". As it is assumed that atomic programs in Atm are linear (i.e., all atomic programs in Atm occurring at a given state lead to the same successor state), [[a]]ϕ can also be read "if the atomic program a occurs, ϕ will be true afterwards". Indeed, from the assumption of linearity, it follows that atomic programs in Atm are deterministic (i.e., there is at most one possible execution of an atomic program a at a given state). Finally, the formula [[≡]]ϕ has to be read "ϕ is true in all histories passing through the current moment" or, more shortly, "ϕ is necessarily true in the current moment".

Semantics

OPDL frames are structures with two dimensions: a vertical dimension corresponding to the concept of history, a horizontal dimension corresponding to the concept of moment.

Definition 1 (OPDL frame).

An OPDL frame is a tuple F = (W, Q, L, R ≡ ) where:

-W is a nonempty set of states (or worlds), -Q is a partial function Q : W -→ W , -L is a mapping L : Z -→ 2
-R ≡ ⊆ W × W is an equivalence relation between states in W such that for all w, v, u ∈ W : (C1) if Q(w) = v and (v, u) ∈ R ≡ then there is z ∈ W such that (w, z) ∈ R ≡ and Q(z) = u and L(z, u) = L(w, v).
For every w, v ∈ W , Q(w) = v means that v is the successor state of w. If Q(w) = v then we also say that w is a predecessor of v. If L(w, v) = {a, b}, then the actions a and b are responsible for the transition from the state w to the state v. In other words, the function L labels every state transition with a set of atomic actions (viz. the actions that are responsible for the transition). The assumption that the set L(w, v) should be nonempty means that every state transition is due to the execution of at least one atomic action. R ≡ -equivalence classes are called moments. If w and v belong to the same moment then they are called alternatives. A maximal sequence of states according to the transition relation Z starting at a given state w is called history starting in w. If w and v belong to the same moment, then the history starting in w and the history starting in v are alternative histories (viz. histories starting at the same moment).

Constraint (C1) corresponds to what in Ockhamist semantics is called property of weak diagram completion [START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF]. This means that if two worlds v and u are in the same moment and world w is a predecessor of v then, there exists a world z such that (i) w and z are in the same moment, (ii) u is the successor of z, (iii) the transition from w to v and the transition from z to u are labeled with the same set of action names. Figure 1 is an example of OPDL frame. The R ≡ -equivalences classes {w 1 , w 2 , w 3 , w 4 }, {w 5 , w 6 }, {w 7 , w 8 }, {w 9 }, {w 10 }, {w 11 }, {w 12 }, {w 13 }, {w 14 }, {w 15 } and {w 16 } are the moments. The sequences of states (w 1 , w 5 , w 9 , w 13 ), (w 2 , w 6 , w 10 , w 14 ), (w 3 , w 7 , w 11 , w 15 ) and (w 4 , w 8 , w 12 , w 16 ) are the alternative histories starting at the same moment {w 1 , w 2 , w 3 , w 4 }. Actions a and c are responsible for the transition from the state w 1 to the state w 5 and, because of Constraint (C1), actions a and c are also responsible for the transition from the state w 2 to the state w 6 . Moreover, actions b and c are responsible for the transition from the state w 3 to the state w 7 and, because of Constraint (C1), actions b and c are also responsible for the transition from the state w 4 to the state w 8 .

Definition 2 (Atomic transitions). Given an OPDL frame

F = (W, Q, L, R ≡ ) and an atomic program a ∈ Atm, let R a = {(w, v) | Q(w) = v and a ∈ L(w, v)} be the set of a-transitions in the frame F .
An OPDL model is an OPDL frame supplemented with a valuation function mapping each state to the set of propositional atoms which are true in it, under the assumption that two states belonging to the same moment agree on the atoms. More precisely:

Definition 3 (OPDL model). An OPDL model is a tuple M = (W, Q, L, R ≡ , V)
where:

Fig. 1. An OPDL frame -(W, Q, L, R ≡ ) is a OPDL frame and -V : W -→ 2 Prop is a valuation function for atomic propositions such that for all w, v ∈ W : (C2) if (w, v) ∈ R ≡ then V(w) = V(v).
The truth of a OPDL formula is evaluated with respect to a world w in an OPDL model M .

Definition 4 (π-transitions and truth conditions). Let

M = (W, Q, L, R ≡ , V)
R π1;π2 = R π1 • R π2 R π1∪π2 = R π1 ∪ R π2 R π * = (R π ) * R ϕ? = {(w, w) | w ∈ W and M, w |= ϕ} and M, w |= p ⇐⇒ p ∈ V(w); M, w |= ¬ϕ ⇐⇒ M, w |= ϕ; M, w |= ϕ ∧ ψ ⇐⇒ M, w |= ϕ AND M, w |= ψ; M, w |= [[π]]ϕ ⇐⇒ ∀v ∈ R π (w) : M, v |= ϕ with R π (w) = {v ∈ W | (w, v) ∈ R π }.
An OPDL formula ϕ is said to be OPDL valid, denoted by |= OPDL ϕ, if and only if ϕ is true in all OPDL models (i.e., for every OPDL model M and for every world w in M , we have M, w |= ϕ). An OPDL formula ϕ is said to be OPDL satisfiable if and only if ¬ϕ is not OPDL valid.

OPDL formulae can also be interpreted over standard Kripke structures.

Definition 5 (Kripke OPDL model

). A Kripke OPDL model is a tuple M = (W, {R a | a ∈ Atm}, R ≡ , V) where:
-W is a set of states (or worlds), -R ≡ is an equivalence relation on W and all R a are binary relations on W satisfying the following two constraints for all w, v, u ∈ W :

(C1 * ) if (w, v) ∈ R X and (w, u) ∈ R X then u = v, (C2 * ) if (w, v) ∈ R X and (v, u) ∈ R ≡ then there is z ∈ W such that (w, z) ∈ R ≡ and for all a ∈ Atm, (w, v) ∈ R a if and only if (z, u) ∈ R a , with R X = a∈Atm R a , -V : W -→ 2 Prop is a valuation function for atomic propositions such that for all w, v ∈ W : (C3 * ) if (w, v) ∈ R ≡ then V(w) = V(v).
Constraints (C2 * ) and (C3 * ) are respectively the counterparts of Constraint (C1) and Constraint (C2) in the definition of an OPDL model. Constraint (C1 * ) forces the successor relation R X to be deterministic (i.e., every state has at most one successor). As stated by the following proposition, the notion of satisfiability with respect to the class of OPDL models is equivalent to the notion of satisfiability with respect to the class of Kripke OPDL models. Proposition 1. Let ϕ be an OPDL formula. Then, there exists an OPDL model which satisfies ϕ if and only if there exists a Kripke OPDL model which satisfies ϕ.

We shall say that ϕ is a global logical consequence of a finite set of global axioms Γ = {χ 1 , . . . , χ n }, denoted by Γ |= OPDL ϕ, if and only if for every OPDL model M , if Γ is true in M (i.e., for every world w in M , we have M, w |= χ 1 ∧ . . . ∧ χ n ) then ϕ is true in M too (i.e., for every world w in M , we have M, w |= ϕ).

As the following proposition highlights, when the set of atomic programs Atm is finite, the problem of logical consequence in OPDL with a finite set of global axioms is reducible to the validity problem for OPDL formulae.

Proposition 2. Let Γ = {χ 1 , . . . , χ n } be a finite set of OPDL formulae. If Atm is finite, Γ |= OPDL ϕ if and only if |= OPDL [[any * ]](χ 1 ∧ . . . ∧ χ n ) → ϕ with any def = ( a∈Atm ∪ ≡).
The model checking problem for OPDL is the following decision problem: given a finite OPDL model M and an OPDL formula ϕ, is there a world in M such that M, w |= ϕ? With finite OPDL model, we mean a OPDL model M = (W, Q, L, R ≡ , V) that satisfies the following three conditions: (1) W is finite; (2) L associates to every transition (w, v) ∈ Z = {(w, v) | w, v ∈ W and Q(w) = v} a non-empty finite set of atomic actions in Atm; (3) V associates to every world w ∈ W a finite set of atomic formulas in Prop. In order to determine whether there exists a world w in M such that M, w |= ϕ, we can use the model checking algorithm for PDL showing that the model checking problem for PDL is PTIME-complete with respect to the size of the input model and the input formula. It follows that the model checking problem for OPDL is PTIME-complete too with respect to size(M ) + size(ϕ).

Decidability of OPDL

Using the "mosaic method", a technique used in algebraic logic [START_REF] Németi | Decidable versions of first order logic and cylindric-relativized set algebras[END_REF] to prove the decidability of equational theories, we will prove the decidability of SAT , the following decision problem: determine whether a given OPDL formula ϕ is satisfiable with respect to the class of OPDL models.

Theorem 1. SAT is decidable.

Proof (Sketch). Let ϕ be a formula. In order to simplify the proof, we assume that at most one atomic action, namely a, occurs in ϕ. A type for ϕ is a subset t of F L(ϕ). It is normal iff it satisfies the conditions of atomicity considered in [14, Definition 2.2]. A group for ϕ is a finite set G of normal types for ϕ. A mosaic for ϕ is a finite set M of groups for ϕ. It is normal iff it satisfies the following conditions:

(i) if p ∈ F L(ϕ) then for all G ∈ M , for all t ∈ G, if p ∈ t then for all H ∈ M , for all u ∈ H, p ∈ u; (ii) if [[≡ ]]ψ ∈ F L(ϕ) then for all G ∈ M , for all t ∈ G, if [[≡]]ψ ∈ t then for all H ∈ M , for all u ∈ H, ψ ∈ u; (iii) if ¬[[≡]]ψ ∈ F L(ϕ) then for all G ∈ M , for all t ∈ G, if ¬[[≡]]ψ ∈ t
then there exists H ∈ M , there exists u ∈ H such that ¬ψ ∈ u. A system for ϕ is a finite set S of normal mosaics for ϕ. A context for S is a structure of the form (M, G, t) where M ∈ S, G ∈ M and t ∈ G. Obviously, there exists finitely many types, groups, mosaics and systems for ϕ. Since the normality conditions for types and mosaics are decidable, the set of all contexts can be computed. Let Σ = {a, ≡}∪{ψ?: ψ ∈ F L(ϕ)}. For all α ∈ Σ, we define the transition relation -→ S α between contexts for S as follows: (M, G, t) -→ S α (N, H, u) iff one of the following conditions is satisfied: (i) α = a and there exists a bijection f :

G → N such that (a) f (t) = u, (b) if [[a]]ψ ∈ F L(ϕ) then for all v ∈ G, if [[a]]ψ ∈ v then ψ ∈ f (v), (c) if ¬[[a]]ψ ∈ F L(ϕ) then for all v ∈ G, if ¬[[a]]ψ ∈ v then ¬ψ ∈ f (v); (ii) α =≡ and M = N ; (iii) α = ψ?, M = N , G = H, t = u and ψ ∈ u.
For all programs π, we inductively define the transition relation -→ S π between contexts for S as follows:

-→ S π1;π2 = -→ S π1 • -→ S π2 , -→ S π1∪π2 = -→ S π1 ∪ -→ S π2 , -→ S π ⋆ = (-→ S π ) ⋆ .
Since the set of all contexts can be computed, the transition relations -→ S π are all decidable. A system S for ϕ is said to be saturated iff it satisfies the following condition

: if ¬[[π]]ψ ∈ F L(ϕ) then for all contexts (M, G, t) for S, if ¬[[π]]ψ ∈ t then there exists a context (N, H, u) for S such that (M, G, t) -→ S π (N, H, u
) and ¬ψ ∈ u. Since the transition relations -→ S π are all decidable, checking the saturation of a given system for ϕ is decidable. The proof of the decidability of SAT proceeds in two steps. First, in Proposition 3, we prove that ϕ is satisfiable iff there exists a saturated system S for ϕ and there exists a context (M, G, t) in S such that ϕ ∈ t. Second, in Proposition 4, we prove the decidability of the decision problem SY S defined as follows: determine whether there exists a saturated system S for a given formula ϕ and there exists a context (M, G, t) in S such that ϕ ∈ t. Proposition 3. Let ϕ be a formula. The following conditions are equivalent: (i) ϕ is satisfiable; (ii) there exists a saturated system S for ϕ, there exists a context (M, G, t) in S such that ϕ ∈ t.

Proposition 4. SY S is decidable.

As a result, SAT is decidable.

⊓ ⊔

Relationships between OPDL, PDL and CTL *

In this section we study the relationships between OPDL and PDL, and between OPDL and CTL * . In particular, we provide a polynomial embedding of PDL into OPDL and a polynomial embedding of CTL * into OPDL.

Relationships between OPDL and PDL

Propositional Dynamic Logic PDL [START_REF] Harel | Dynamic Logic[END_REF] is the well-known logic of programs. Again assume the countable set of atomic propositions Prop = {p, q, . . .} and the countable set of atomic programs Atm = {a, b, . . .}. The language L PDL (Prop, Atm) of PDL is defined by the following grammar in Backus-Naur Form (BNF):

Prg : π ::= a | (π 1 ; π 2 ) | (π 1 ∪ π 2 ) | π * | ϕ? Fml : ϕ ::= p | ¬ϕ | (ϕ 1 ∧ ϕ 2 ) | [π]ϕ
where p ranges over Prop and a ranges over Atm. PDL models are nothing but labeled transition systems, i.e., transition systems where transitions between states are labeled with atomic programs. Definition 6. PDL models are tuples M = (W, {R a | a ∈ Atm}, V) where:

-W is a nonempty set of possible worlds or states; -{R a | a ∈ Atm} is a set of binary relations on W ; -V : W -→ 2 Prop is a valuation function.

The accessibility relations for atomic programs are generalized to complex programs in the usual way (see Definition 2).

The truth conditions of PDL formulae are standard for the Boolean constructions plus the following one for the dynamic operators [π]:

M, w |= [π]ϕ ⇐⇒ ∀v ∈ R π (w) : M, v |= ϕ
A PDL formula ϕ is said to be PDL valid if and only if ϕ is true in all PDL models.

We can embed PDL in OPDL. Consider the following polynomial translation tr 1 : L PDL (Prop, Atm) -→ L OPDL (Prop, Atm) from the language of PDL to the OPDL language.

tr 1 (p) = p for all p ∈ Prop tr 1 (¬ϕ) = ¬tr 1 (ϕ) tr 1 (ϕ 1 ∧ ϕ 2 ) = tr 1 (ϕ 1 ) ∧ tr 1 (ϕ 2 ) tr 1 ([π]ϕ) = [[tr 2 (π)]]tr 1 (ϕ)
where tr 2 (a) = ≡; a for all a ∈ Atm tr 2 (π 1 ; π 2 ) = tr 2 (π 1 ); tr 2 (π 2 )

tr 2 (π 1 ∪ π 2 ) = tr 2 (π 1 ) ∪ tr 2 (π 2 ) tr 2 (π * ) = (tr 2 (π)) * tr 2 (ϕ?)
= tr 1 (ϕ)?

As the following theorem shows, the preceding translation is a correct embedding.

Theorem 2. Let ϕ be a PDL formula. ϕ is PDL valid if and only if tr 1 (ϕ) is OPDL valid.

Relationships between OPDL and CTL *

Full Computation Tree Logic CTL * was first described in [START_REF] Emerson | Deciding full branching time logic[END_REF][START_REF] Emerson | Sometimes' and 'not never' revisited: on branching versus linear time[END_REF] as an extension of Computation Tree Logic CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF] and Propositional Linear Temporal Logic PLTL [START_REF] Pnueli | The temporal logic of programs[END_REF]. The language of CTL * is built recursively from the atomic propositions using the temporal operators of PLTL, and the existential path switching operator of CTL as well as classical connectives. Again assume the countable set of atomic propositions Prop = {p, q, . . .}. The language L CTL * (Prop) of CTL * is defined by the following grammar in Backus-Naur Form (BNF):

ϕ ::= p | ¬ϕ | (ϕ 1 ∧ ϕ 2 ) | Xϕ | ϕ U ψ | Aϕ
where p ranges over Prop. The constructs X and U are respectively the operators next and until of PLTL, the formulas Xϕ and ϕ U ψ being respectively read "ϕ will be true in the next state along the current path" and "ψ will be true at some point in the future along the current path and ϕ has to hold until ψ". These two operators can be used to express other kinds of temporal notions such as eventually Fψ def = ⊤ U ψ, henceforth Gψ def = ¬F¬ψ and before ϕ B ψ def = ¬(¬ϕ U ψ). The construct A is a modal operator quantifying over possible paths, the formula Aϕ being read "ϕ is true in all possible paths". The existential path-quantifier operator E, is defined by Eϕ def = ¬A¬ϕ. Different semantics for CTL * have been given in the literature. One of this semantics is based on the notion of Ockhamist structure. Here we mainly follow the presentation of the Ockhamist semantics for CTL * given by Reynolds [START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF] who introduces a special kind of Ockhamist structures called (N × W ) structures.

Definition 7. A (N × W ) structure is a tuple (W, ∼, g) where:
-W is a set of points; -∼ is an equivalence relation over N × W such that for all w, v ∈ W and for all n, m ∈ N:

(S1) if (n, w) ∼ (m, v) then n = m, (S2) if (n, w) ∼ (n, v) and m < n then (m, w) ∼ (m, v), (S3) (0, w) ∼ (0, v); -g : N × W -→ 2
Prop is a valuation function mapping each integer and each point into a set of atoms such that for all w, v ∈ W and for all n ∈ N: (S4) if (n, w) ∼ (n, v) then g(n, w) = g(n, v). Given a (N × W ) structure (W, ∼, g) and a CTL * formula ϕ, (W, ∼, g), (n, w) |= ϕ means that ϕ is true at the index (n, w) in the (N × W ) structure (W, ∼, g). The rules defining the truth conditions of CTL * formulae are inductively defined as follows:

(W, ∼, g), w) |= p ⇐⇒ p ∈ g(n, w); (W, ∼, g), (n, w) |= ¬ϕ ⇐⇒ (W, ∼, g), (n, w) |= ϕ; (W, ∼, g), (n, w) |= ϕ1 ∧ ϕ2 ⇐⇒ (W, ∼, g), (n, w) |= ϕ1 AND (W, ∼, g), (n, w) |= ϕ2; (W, ∼, g), (n, w) |= Xϕ ⇐⇒ (W, ∼, g), (n + 1, w) |= ϕ (W, ∼, g), (n, w) |= ϕ U ψ ⇐⇒ ∃m ∈ N : m ≥ n AND (W, ∼, g), (m, w) |= ψ AND ∀k ∈ N : IF n ≤ k < m THEN (W, ∼, g), (k, w) |= ϕ (W, ∼, g), (n, w) |= Aϕ ⇐⇒ ∀v ∈ W : IF (n, w) ∼ (n, v) THEN (W, ∼, g), (n, v) |= ϕ
As shown by Reynolds [START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF] the CTL * semantics in terms of (N × W ) structures is equivalent to the CTL * semantics in terms of bundled trees. However, it is more general than the common CTL * semantics in terms of R-generable models used by [START_REF] Emerson | Sometimes' and 'not never' revisited: on branching versus linear time[END_REF], i.e., Kripke structures with states, a total accessibility relation R between them and the set of all paths which arise by moving from state to state along the accessibility relation. The difference between the CTL * semantics in terms of bundled trees and the CTL * semantics in terms of R-generable models is that the latter quantifies over all paths induced by the relation R whereas the former quantifies over a bundle of paths. Although this bundle is suffix and fusion closed, it does not need to be be limit closed. For example, it may be the case that all paths include a right branch even though at every world there is a path where the next branch goes left, which violates the limit closure property. In order to distinguish full computation tree logic interpreted over R-generable models and full computation tree logic interpreted over bundled trees (and equivalently over (N × W ) structures), some authors (see, e.g., [START_REF] Reynolds | A tableau for bundled CTL*[END_REF][START_REF] Masini | Labelled natural deduction for a bundled branching temporal logic[END_REF][START_REF] Mccabe-Dansted | A tableau for the combination of CTL and BCTL[END_REF]) use the term CTL * to indicate the former logic and the term BCTL * (bundled CTL * ) to indicate the latter (in [START_REF] Stirling | Modal and temporal logics[END_REF] it is called ∀LTFC ).

It is well-known that CTL * interpreted over R-generable models is 2-EXPTIME complete: [START_REF] Emerson | Deciding full branching time logic[END_REF] provides a doubly exponential automaton based satisfiability checker, and [START_REF] Vardi | Improved upper and lower bounds for modal logics of programs[END_REF] gives a lowerbound. As pointed by [START_REF] Mccabe-Dansted | A tableau for the combination of CTL and BCTL[END_REF], an argument for the 2-EXPTIME hardness of the satisfiability problem could also be made for CTL * interpreted over bundled trees in a way similar to the argument for CTL * interpreted over R-generable models. Therefore, as the CTL * semantics in terms of bundled trees is equivalent to the CTL * semantics in terms of (N × W ) structures [START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF], it follows that the satisfiability problem for CTL * interpreted over (N×W ) structures is also 2-EXPTIME hard. Therefore, CTL * interpreted over bundled trees (or over (N × W ) structures) is not easier to deal with than CTL * interpreted over R-generable models. However, one interesting aspect of the former kind of CTL * is that it is closely connected to Ockhamist temporal logics studied in the field of philosophical logic [START_REF] Zanardo | Branching-time logic with quantification over branches: The point of view of modal logic[END_REF]. Moreover, one might argue that reasoning in BCTL * is relatively easier than reasoning in CTL * . For example the specification for the tableau method for BCTL * proposed by [START_REF] Reynolds | A tableau for bundled CTL*[END_REF] was much simpler than the CTL * tableau that originated from it [START_REF] Reynolds | A tableau for CTL*[END_REF].

Consider the following translation tr 3 : L CTL * (Prop) -→ L OPDL (Prop, Atm) from the language of CTL * to the OPDL language where x is an arbitrary atomic program in Atm:

tr 3 (p) = p for all p ∈ Prop tr 3 (¬ϕ) = ¬tr 3 (ϕ) tr 3 (ϕ 1 ∧ ϕ 2 ) = tr 3 (ϕ 1 ) ∧ tr 3 (ϕ 2 ) tr 3 (Xϕ) = x tr 3 (ϕ) tr 3 (ϕ U ψ) = (tr 3 (ϕ)?; x) * tr 3 (ψ) tr 3 (Aϕ) = [[≡]]tr 3 (ϕ)
The preceding translation is polynomial and, as the following theorem shows, it provides an embedding of the variant of CTL * interpreted over (N × W ) structures into OPDL.

Theorem 3. Let ϕ be a CTL * formula. ϕ is valid with respect to the class of (N × W ) structures if and only if { x ⊤} |= OPDL tr 3 (ϕ).

From Theorem 3 and Proposition 2 in Section 2.2, it follows that the satisfiability problem in the variant of CTL * interpreted over (N × W ) structures can be reduced to the satisfiability problem in OPDL with a finite number of atomic programs. Since the satisfiability problem of (N × W ) structures is 2-EXPTIME-hard (see above), the preceding polynomial embedding of CTL * into OPDL provides an argument for the 2-EXPTIME-hardness of the satisfiability problem of our logic OPDL.

Relationships with Other Logics: Discussion

The logic OPDL has interesting connections with other logical systems proposed in the field of theoretical computer science such as propositional linear time temporal logic PLTL and Nishimura's combination of PDL and PLTL (call it, NL) [START_REF] Nishimura | Descriptively complete process logic[END_REF]. As for PLTL, in the previous Section 3.2 we have provided a polynomial embedding of CTL * into OPDL. As PLTL is nothing but the fragment of CTL * without the path quantifier operator A, the translation tr 3 also provides a polynomial embedding of PLTL into OPDL. As for NL, we just need to put together the translation tr 1 from PDL to OPDL given in Section 3.1 and the translation from PLTL to OPDL in order to provide a polynomial reduction of Nishimura's logic NL to OPDL. Another logic that is related with OPDL is ACTL * , the action based version of CTL * proposed by [START_REF] De Nicola | Action versus state based logics for transition systems[END_REF]. ACTL * extends CTL * with temporal operators X a indexed by atomic programs a in the set of atomic programs Atm. The ACTL * formula X a ϕ has to be read "the next transition is labeled with the atomic program a and ϕ will be true in the next state along the current path". By adding the following item to the preceding translation tr 3 from CTL * to OPDL, we get a polynomial embedding of ACTL * into OPDL: tr 3 (X a ϕ) = a tr 3 (ϕ) for all a ∈ Atm As we have shown in Section 3.2, the logic OPDL interpreted over OPDL models (Definition 3) embeds the variant of CTL * interpreted over (N × W ) structures which in turn is equivalent to the variant of CTL * interpreted over bundled trees.

A second variant of CTL * , first introduced by [START_REF] Emerson | Sometimes' and 'not never' revisited: on branching versus linear time[END_REF], is the one interpreted over Rgenerable models of the form M = (W, R, V) where W is a set of states, R ⊆ W × W is a total binary relation on W (i.e., for every w ∈ W , there is some v ∈ W such that (w, v) ∈ R) and V : W -→ 2 Prop is a valuation function for atomic propositions. 3Given a model M = (W, R, V), a fullpath in M is defined to be an infinite sequence (w 1 , w 2 , w 3 , . . .) of states of M such that for each i ≥ 1, (w i , w i+1 ) ∈ R. Given a fullpath σ = (w 1 , w 2 , w 3 , . . .) and an integer i ≥ 1, the symbol σ ≥i denotes the fullpath (w i , w i+1 , . . .). As usual, σ [START_REF] Alur | Alternating-time temporal logic[END_REF] denotes the first element of the sequence σ. Truth of a CTL * formula is evaluated with respect to a R-generable model M and a fullpath σ in M . Specifically, the rules defining the truth conditions of CTL * formulae are inductively defined as follows:

M, σ |= p ⇐⇒ p ∈ V(σ[1]); M, σ |= ¬ϕ ⇐⇒ M, σ |= ϕ; M, σ |= ϕ1 ∧ ϕ2 ⇐⇒ M, σ |= ϕ1 AND M, σ |= ϕ2; M, σ |= Xϕ ⇐⇒ M, σ ≥2 |= ϕ M, σ |= ϕ U ψ ⇐⇒ ∃i ≥ 1 : M, σ ≥i |= ψ AND ∀j : IF 1 ≤ j < i THEN M, σ ≥j |= ϕ M, σ |= Aϕ ⇐⇒ ∀σ ′ : IF σ[1] = σ ′ [1] THEN M, σ ′ |= ϕ
Here we consider a variant of OPDL which embeds the preceding variant of CTL * interpreted over R-generable models. We call OPDL lts this variant of OPDL, where OPDL lts means 'OPDL interpreted over labeled transition systems'. The semantics for OPDL lts is given in terms of PDL models as defined in Section 3.1 (Definition 6), which are nothing but labeled transition systems, i.e., transition systems where transitions between states are labeled with atomic programs. Given a PDL model M = (W, {R a | a ∈ Atm}, V), let the successor state function succ be defined by succ(w) = a∈Atm {v ∈ W | (w, v) ∈ R a } for each w ∈ W . succ(w) identifies the successors of world w in M . Moreover, for every w ∈ W , let PA ={(w 1 , . . . , w n ) | w 1 , . . . , w n ∈ W and w i+1 = succ(w i ) for all 1 ≤ i < n} be the set of all paths in M . For every w ∈ W , let MPA w be the set of all maximal paths starting in w, also called histories starting in w. That is, σ ∈ MPA w if and only if σ ∈ PA and σ[1] = w and there is no σ ′ ∈ PA such that σ ′ [1] = w and σ ⊏ σ ′ (i.e., σ is a proper initial subsequence of σ ′ ). Finally, let IN = {w/σ | w ∈ W and σ ∈ MPA w } be the set of all indexes in the model M .

Truth of an OPDL formula is evaluated at a given index w/σ ∈ IN of a PDL model M . The rules inductively defining the truth conditions of OPDL formulae are:

M, w/σ |= p ⇐⇒ p ∈ V(w); M, w/σ |= ¬ϕ ⇐⇒ M, w/σ |= ϕ; M, w/σ |= ϕ ∧ ψ ⇐⇒ M, w/σ |= ϕ AND M, w/σ |= ψ; M, w/σ |= [[π]]ϕ ⇐⇒ ∀ v/σ ′ ∈ ρ π (w/σ) : M, v/σ ′ |= ϕ where ρ a = {(w/σ, v/σ ′ ) | w/σ, v/σ ′ ∈ IN , (w, v) ∈ R a and σ = (w, σ ′ )} ρ ≡ = {(w/σ, v/σ ′ ) | w/σ, v/σ ′ ∈ IN and w = v} ρ π1;π2 = ρ π1 • ρ π2 ρ π1∪π2 = ρ π1 ∪ ρ π2 ρ π * = (ρ π ) * ρ ϕ? = {(w/σ, w/σ) | w/σ ∈ IN and M, w/σ |= ϕ} and ρ π (w/σ) = {v/σ ′ | (w/σ, v/σ ′ ) ∈ ρ π }.
A formula ϕ of the language L OPDL (Prop, Atm) is said to be OPDL lts valid, denoted by |= OPDL lts ϕ, if and only if ϕ is true in all PDL models. As usual, a formula ϕ of the language L OPDL (Prop, Atm) is said to be OPDL lts satisfiable if and only if ¬ϕ is not OPDL lts valid. We shall say that a formula ϕ of the language L OPDL (Prop, Atm) is a global logical consequence in OPDL lts of a finite set of global axioms Γ = {χ 1 , . . . , χ n }, denoted by Γ |= OPDL lts ϕ, if and only if for every PDL model M , if Γ is true in M then ϕ is true in M too.

As the following theorem shows, the translation given in Section 3.2 provides an embedding of the variant of CTL * interpreted over R-generable models into OPDL lts . Theorem 4. Let ϕ be a CTL * formula. ϕ is valid with respect to the class of Rgenerable models if and only if { x ⊤} |= OPDL lts tr 3 (ϕ).

From Theorem 4 and the fact that, as in OPDL, the problem of global logical consequence in OPDL lts with a finite number of global axioms is reducible to the problem of OPDL lts validity, it follows that the satisfiability problem in the variant of CTL * interpreted over R-generable models can be reduced to the satisfiability problem in OPDL lts with a finite number of atomic programs. Corollary 2. Let ϕ be a CTL * formula and let Atm be finite. ϕ is valid with respect to the class of R-generable models if and only if |= OPDL lts [[any * ]] x ⊤ → tr 3 (ϕ).

Perspectives

We have presented a new logic called Ockhamist Propositional Dynamic Logic OPDL and studied its relationship with PDL and CTL * . An interesting issue for future research is the study of the relationship between OPDL and PDL with intersections of programs. Intersections of atomic programs can be simulated in OPDL as follows:

[[a ∩ b]]ϕ def = [[≡]]( a ⊤ → [[b]]ϕ)
However, it is not clear whether we can find a simple translation from PDL with intersection of (not necessarily atomic) programs to OPDL that preserves validity.

Another direction of future research is the study of the exact complexity of the satisfiability problem for OPDL. The embedding of CTL * into OPDL ensures that it is 2-EXPTIME hard. However, the construction based on the "mosaic method" given in the Section 2.3 does not provide an optimal decision procedure for OPDL. Future work will be devoted to find an optimal decision procedure for OPDL showing that its satisfiability problem is in 2-EXPTIME. Indeed, at the current stage, we conjecture that CTL * is not easier to deal with than OPDL. We also plan to find a sound and complete axiomatization for the logic OPDL.

As to the logic OPDL lts whose semantics has been sketched in Section 4, much work remains to be done. First of all, we plan to study more in detail the differences between OPDL and OPDL lts , taking inspiration from Reynolds' work [START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF] on the comparison between the CTL * semantics in terms of R-generable models and the CTL * semantics in terms of (N × W ) structures (or bundled trees). For instance, we plan to find some interesting examples of formulae of the language L OPDL (Prop, Atm) which are valid in OPDL lts but are not valid in OPDL. Secondly, we plan to adapt the proof of the decidability of the satisfiability problem for OPDL given in the Section 2.3 in order to prove the decidability of the satisfiability problem for OPDL lts . Another aspect of the logic OPDL lts that we plan to investigate in the future is its relationship with the extension of PDL with a repetition construct (PDL-∆) by [START_REF] Streett | Propositional dynamic logic of looping and converse is elementarily decidable[END_REF]. PDL-∆ extends PDL with constructions of the form ∆π meaning that "the program π can be repeatedly executed infinitely many times". We believe that the construction ∆π can be simulated in OPDL lts as follows:

∆π def = ≡ [[π * ]] π ⊤
We postpone to future work the definition of the exact translation from PDL-∆ formulae to OPDL lts formulae and a theorem stating that, for every PDL-∆ formula ϕ, ϕ is PDL-∆ valid if and only if the translation of ϕ in OPDL lts is OPDL lts valid.

  Atm * from state transitions to non-empty sets of atomic programs, Z = {(w, v) | w, v ∈ W and Q(w) = v} being the transition relation induced by the successor state function Q,

Corollary 1 .

 1 Let ϕ be a CTL * formula and let Atm be finite. ϕ is valid with respect to the class of (N × W ) structures if and only if |= OPDL [[any * ]] x ⊤ → tr 3 (ϕ).

It is worth noting that Axelsson et al.[START_REF] Axelsson | Extended computation tree logic[END_REF] have recently studied generic extensions of CTL in which temporal operators are parameterized with different kinds of formal languages recognized by different classes of automata (e.g., regular languages, visibly pushdown and contextfree languages). They compare the expressive power of these extensions of PDL to CTL, PDL and extensions of PDL such as PDL-∆. However, they also show that CTL * cannot be embedded in any of these extensions of CTL, as the property of fairness is expressible in CTL * but is not expressible is any of these logics (see[START_REF] Axelsson | Extended computation tree logic[END_REF] Theorem 4.

3]).[START_REF] Axelsson | Extended computation tree logic[END_REF] An extended version of this paper containing detailed proofs is available at[START_REF] Balbiani | Ockhamist propositional dynamic logic: a natural link between PDL and CTL[END_REF].

It has been proved that the variant of CTL * interpreted over (N×W ) structures is more general than the variant of CTL * interpreted R-generable models, in the sense that the former have less validities than the latter. For instance, as shown by[START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF], the formula AG(p → EXp) → (p → EGp) is valid in the latter variant of CTL * but is not valid in the former.