2014 RefinementModalLogic

• (Bozzelli et al., 2014) ⇒ Laura Bozzelli, Hans van Ditmarsch, Tim French, James Hales, and Sophie Pinchinat. (2014). “Refinement Modal Logic.” In: Information and Computation Journal, 239(C). doi:10.1016/j.ic.2014.07.013

Subject Headings: Refinement Modal Logic, Multi-agent Modal Logic System, Multi-agent Refinement Modal Logic, Dynamic Epistemic Logic.

Notes

• Copyright: Open Archive article distributed under an Elsevier user license.

Cited By

• Google Scholar: ~ 26 Citations
• DL- ACM: ~ 4 Citations
• Elsevier ScienceDirect: ~ 13 Citations
• Semantic Scholar ~ 10 Citations

Quotes

Abstract

In this paper we present refinement modal logic. A refinement is like a bisimulation, except that from the three relational requirements only 'atoms' and 'back' need to be satisfied. Our logic contains a new operator [math]\displaystyle{ \forall }[/math] in addition to the standard box modalities for each agent. The operator [math]\displaystyle{ \forall }[/math] acts as a quantifier over the set of all refinements of a given model. As a variation on a bisimulation quantifier, this refinement operator or refinement quantifier [math]\displaystyle{ \forall }[/math] can be seen as quantifying over a variable not occurring in the formula bound by it. The logic combines the simplicity of multi-agent modal logic with some powers of monadic second-order quantification. We present a sound and complete axiomatization of multi-agent refinement modal logic. We also present an extension of the logic to the modal µ-calculus, and an axiomatization for the single-agent version of this logic. Examples and applications are also discussed: to software verification and design (the set of agents can also be seen as a set of actions), and to dynamic epistemic logic. We further give detailed results on the complexity of satisfiability, and on succinctness.

1. Introduction

Modal logic is frequently used for modelling knowledge in multi-agent systems. The semantics of modal logic uses the notion of “possible worlds”, between which an agent is unable to distinguish. In dynamic systems agents acquire new knowledge (say by an announcement, or the execution of some action) that allows agents to distinguish between worlds that they previously could not separate. From the agent's point of view, what were “possible worlds” become inconceivable. Thus, a future informative event may be modelled by a reduction in the agent's accessibility relation. In [55] the future event logic is introduced. It augments the multi-agent logic of knowledge with an operation ∀φ that stands for “φ holds after all informative events” — the diamond version ∃φ stands for “there is an informative event after which φ.” The proposal was a generalization of a so-called arbitrary public announcement logic with an operator for “φ holds after all announcements” [8]. The semantics of informative events encompasses action model execution à la Baltag et al. [9]: on finite models, it can be easily shown that a model resulting from action model execution is a refinement of the initial model, and for a given refinement of a model we can construct an action model such that the result of its execution is bisimilar to that refinement. In [56] an axiomatization of the single-agent version of this logic is presented, and also expressivity and complexity results. These questions were visited in both the context of modal logic, and of the modal μ-calculus.

In the original motivation, the main operator ∃ had a rather temporal sense — therefore the ‘future event’ name. However, we have come to realize that the structural transformation that interprets this operator is of much more general use, on many very different kinds of modal logic, namely anywhere where more than a mere model restriction or pruning is required. We have therefore come to call this the refinement operator, and the logic refinement modal logic.

Thus we may consider refinement modal logic to be a more abstract perspective of future event logic [55] applicable to other modal logics. To any other modal logic! This is significant in that it motivates the application of the new operator in many different settings. In logics for games [42], [2] or in control theory [47], [51], it may correspond to a player discarding some moves; for program logics [29] it may correspond to operational refinement [40]; and for logics for spatial reasoning it may correspond to sub-space projections [41].

Let us give an example. Consider the following structure. The [math]\displaystyle{ \circ }[/math] state is the designated point. The arrows can be associated with a modality.

E.g., [math]\displaystyle{ \Diamond \Diamond \Diamond \;\square \perp }[/math] is true in the point. From the point of view of the modal language, this structure is essentially the same structure (it is bisimilar) as

This one also satisfies [math]\displaystyle{ \Diamond \Diamond \Diamond \;\square \perp }[/math] and any other modal formula for that matter. A more radical structural transformation would be to consider submodels, such as

A distinguishing formula between the two is [math]\displaystyle{ \Diamond \Diamond \;\square \perp }[/math], which is true here and false above. Can we consider other ‘submodel-like’ transformations that are neither bisimilar structures nor strict submodels? Yes, we can. Consider

It is neither a submodel of the initial structure, nor is it bisimilar. It satisfies the formula [math]\displaystyle{ \Diamond \Diamond \;\square \perp \wedge \Diamond \Diamond \Diamond \;\square \perp }[/math]that certainly is false in any submodel. We call this structure a refinement (or ‘a refinement of the initial structure’), and the original structure a simulation of the latter. Now note that if we consider the three requirements ‘atoms’, ‘forth’, and ‘back’ of a bisimulation, that ‘atoms’ and ‘back’ are satisfied but not ‘forth’, e.g., from the length-three path in the original structure the last arrow has no image. There seems to be still some ‘submodel-like’ relation with the original structure. Look at its bisimilar duplicate (the one with seven states). The last structure is a submodel of that copy. Such a relation always holds: a refinement of a given structure can always be seen as the model restriction of a bisimilar copy of the given structure. This work deals with the semantic operation of refinement, as in this example, in full generality, and also applied to the multi-agent case.

Previous works [19], [37] employed a notion of refinement. In [37] it was shown that model restrictions were not sufficient to simulate informative events, and they introduced refinement trees for this purpose — a precursor of the dynamic epistemic logics developed later (for an overview, see [57]). This usage of refinement as a more general operation than model restriction is similar to ours.

In formal methods literature, see e.g. [62], refinement of datatypes is considered such that (datatype) C refines A if A simulates C. This usage of refinement as the converse of simulation [1], [11] comes close to ours — in fact, it inspired us to propose a similar notion, although the correspondence is otherwise not very close. A similar usage of refinement as in [62] is found in [3], [4]. In the theory of modal specifications a refinement preorder is used, known as modal refinement [45], [49]. Modal specifications are deterministic automata equipped with may-transitions and must-transitions. A must-transition is available in every component that implements the modal specification, while a may-transition need not be. This is close to our definition of refinement, as it also is some kind of submodel quantifier, but the two notions are incomparable, because ‘must’ is a subtype of ‘may’.

We incorporate implicit quantification over informative events directly into the language using, again, a notion of refinement; also in our case a refinement is the converse of simulation. Our work is closely related to some recent work on bisimulation quantified modal logics [17], [22]. The refinement operator, seen as refinement quantifier, is weaker than a bisimulation quantifier [55], as it is only based on simulations rather than bisimulations, and as it only allows us to vary the interpretation of a propositional variable that does not occur in the formula bound by it. Bisimulation quantified modal logic has previously been axiomatized by providing a provably correct translation to the modal μ-calculus [16]. This is reputedly a very complicated one. The axiomatization for the refinement operator, in stark contrast, is quite simple and elegant.

Overview of the paper

Section 2 gives a wide overview of our technical apparatus: modal logic, cover logic, modal μ-calculus, and bisimulation quantified logic. Section 3 introduces the semantic operation of refinement. This includes a game and (modal) logical characterization. Then, in Section 4, we introduce two logics with a refinement quantifier that is interpreted with the refinement relation: refinement modal logic and refinement μ-calculus. Section 5 contains the axiomatization of that refinement modal logic and the completeness proof. We demonstrate that it is equally expressive as modal logic. We mention results for model classes and . Section 6 gives the axiomatization of refinement μ-calculus. Again, we have a reduction here, to standard μ-calculus. In Section 7 we show that, although the use of refinement quantification does not change the expressive power of the logics, they do make each logic exponentially more succinct. We give a non-elementary complexity bound for refinement modal μ-calculus.

2. Technical Preliminaries

Throughout the paper we assume a finite set of agents A and a countable set of propositional variables P as background parameters when defining the structures and the logics. Agents are named , and propositional variables are . Agent a is assumed female, and b male.

Structures

A model consists of a domain S of (factual) states (or worlds), an accessibility function , and a valuation . States are A pair consisting of a model M (with domain S) and a state is called a pointed model, for which we write . For we write ; accessibility function R can be seen as a set of accessibility relations , and V as a set of valuations . Given two states in the domain, means that in state s agent a considers a possibility. We will also use a relation simply as a set of pairs , and use the abbreviation . As we will be often required to discuss several models at once, we will use the convention that , , etc. The class of all models (given parameter sets of agents A and propositional variables P) is denoted . The class of all models where for all agents the accessibility relation is reflexive, transitive and symmetric is denoted , and the model class with a serial, transitive and Euclidean accessibility relation is denoted .

The restriction of a model M, notation , is a model such that , for each , , and for each , .

Multi-agent modal logic

The language of multi-agent modal logic is inductively defined as where and . Without the construct we get the language of propositional logic. Standard abbreviations are: iff , iff , ⊤ iff , ⊥ iff , and ◇

iff . If there is a single agent only  we may write □φ instead of . Formula variables are  and for sets of formulas we write  For a finite set Φ of  formulas we let the cover operator  be an abbreviation for

◇

we note is always false, whilst is always true.

Let a finite set of formulas and a formula φ with possible occurrences of a propositional variable p be given. Let denote the substitution of all occurrences of p in φ by ψ. Then abbreviates , and similarly stands for and stands for . For example, ◇

abbreviates

◇ , and the definition of , above, is then written as ◇ .

We now define the semantics of modal logic. Assume a model . The interpretation of is defined by induction. A formula φ is valid on a model M, notation , iff for all , ; and φ is valid iff φ is valid on all M (in the model class , given agents A and basic propositions P). The set of validities, i.e., the logic in the stricter sense of the word, is called .

Cover logic

The cover operator ∇ has also been used as a syntactic primitive in modal logics [16]. It has recently been axiomatized [10]. The language of cover logic is defined as where , and . The semantics of is the obvious one if we recall our introduction by abbreviation of the cover operator: The set of validities of cover logic is called . The conjunction of two cover formulas is again equivalent to a cover formula: The modal box and diamond are definable as iff , and ◇ iff , respectively. Cover logic is equally expressive as modal logic (also in the multi-agent version) [10], [34]. We use cover operators in the presentation of the axioms.

Modal μ-calculus

For the modal μ-calculus, apart from the set of propositional variables P we have another parameter set X of variables to be used in the fixed-point construction. The language of modal μ-calculus is defined as follows. where , , , and where in the variable x only occurs positively (i.e. in the scope of an even number of negations) in the formula φ. We will refer to a variable x in an expression as a fixed-point variable. The formula is an abbreviation for . Here, we extend the notion of substitution to modal μ-calculus by ruling out the substitution of bound variables, i.e., to give the crucial clauses: whereas .

For the semantics of the μ-calculus, the valuation V of propositional variables is extended to include fixed-point variables. We write for the operation that changes a given valuation V into one wherein (where ) and the valuation of all other fixed-point and propositional variables remains the same. Given a model , we similarly write for the model . The semantics of (the top-down presentation, not the bottom-up presentation) is now as follows: Let and model M be given.

Disjunctive formula

An important technical definition we require later on is that of a disjunctive formula. A disjunctive formula is specified by the following abstract syntax: (1) where , (propositional logic), and . To get the disjunctive formula (of modal logic) we omit the clauses containing μ-calculus variables x: If the context of the logic is clear, we simply write disjunctive formula (or df). If , we have that , as expected. (2a) (2b)

Bisimulation quantified modal logic

The language is defined as where and . We let abbreviate . We write and for the bisimulation quantifiers in order to distinguish them from the refinement quantifiers ∀ and ∃, to be introduced later. Given an atom p and a formula φ, the expression means that there exists a denotation of propositional variable p such that φ. It is interpreted as follows (restricted bisimulation is introduced further below in Definition 1): In [22, Lemma 2.43] a bisimulation quantifier characterization of fixed points is given (the details of which are deferred to Section 6 on refinement μ-calculus, where they are pertinent), and from [15] we know that bisimulation quantifiers are also expressible in the modal μ-calculus. For more information on the modal μ-calculus, see [16], [58].

3. Refinement

In this section we define the notion of structural refinement, investigate its properties, give a game characterization in (basic) modal logic, and compare refinement to bisimulation and other established semantic notions in the literature.

3.1. Refinement and its basic properties

Definition 1 Bisimulation, simulation, refinement

Let two models and be given. A non-empty relation is a bisimulation if for all and : atoms

iff  for all ;

forth-a for all , if, then there is a such that and ;

back-a for all , if, then there is a such that and .

We write (M and are bisimilar) iff there is a bisimulation between M and , and we write (and are bisimilar) iff there is a bisimulation between M and linking s and . A restricted bisimulation is a bisimulation that satisfies atoms for all variables except p. A total bisimulation is a bisimulation such that all states in the domain and codomain occur in a pair of the relation.

A relation that satisfies atoms, back-a, and forth-a for every , and that satisfies atoms, and back-b for every , is a B-refinement, we say that refines for group of agents B, and we write .1 An A-refinement we call a refinement (plain and simple) and for -refinement we write a-refinement.

Dually to refinement, we similarly define B-simulation . I.e., a relation that satisfies atoms, back-a, and forth-a for every , and that satisfies atoms, and forth-b for every , is a B-simulation.

Restricted refinement and restricted simulation are defined similarly to restricted bisimulation.

The definition of simulation varies slightly from the one given by Blackburn et al. [11, p. 110]. Here we ensure that simulations (and refinements) preserve the interpretations (i.e., the truth and falsity) of atoms, whereas [11] has them only preserve the truth of propositional variables in a simulation — and presumably preserve their falsity in a refinement. We prefer to preserve the entire interpretation, as we feel it suits our applications better. For example, in the case where refinement represents information change, we would not wish basic facts to become false in the process. The changes are supposed to be merely of information, and not factual. Another, inessential, difference with [11] is that in their case atoms and forth are required for all modalities (in the similarity type), i.e., they consider for only.

If is a B-refinement, then the converse relation is a B-simulation, and if refines then we can also say that simulates .

In an epistemic setting a refinement corresponds to the diminishing uncertainty of agents. This means that there is a potential decrease in the number of states and transitions in a model. On the other hand, the number of states as a consequence of refinement may also increase, because the uncertainty of agents over the extent of decreased uncertainty in other agents may still increase. This is perhaps contrary to the concept of program refinement [40] where detail is added to a specification. However, in program refinement the added detail requires a more detailed state space (i.e., extra atoms) and as such is more the domain of bisimulation quantifiers, rather than refinement quantification. Still, the consequence of program refinement is a more deterministic system which agrees with the notion of diminishing uncertainty. Proposition 2

The relation is reflexive and transitive (a pre-order), and satisfies the Church–Rosser property.

Proof

Reflexivity follows from the observation that the identity relation satisfies atoms, and back-a and forth-a for all agents a, and therefore also the weaker requirement for refinement. Similarly, given two a-refinements , and , we can see that their composition, is also an a-refinement. This is sufficient to demonstrate transitivity. The Church–Rosser property states that if and, then there is some model such that and . From Definition 1 it follows that and must be bisimilar to one another with respect to . We may therefore construct such a model by taking (or ) and setting and for all . It can be seen that , where and , satisfies the required properties.  □

An elementary result is the following. Proposition 3

Let , and let and be given. Then iff .

Example 4

If and , it is not necessarily the case that . For example, consider the one-agent models M and N where: • , and for all ; and

• , and for all .

These two models are clearly not bisimilar, although via and via . See Fig. 1.

Download full-size image Fig. 1. Refinement and simulation, but no bisimulation.

Given that the equivalence defined by and is not a bisimulation, an interesting question seems to be what it then represents. It seems to formalize that two structures are only different in resolvable differences in uncertainty (for the agent of the refinement), but not in hard and necessary facts. So the positive formulas (for that agent) should be preserved under this ‘equivalence’ ≡. Such matters will now be addressed.

3.2. Game and logical characterization of refinement

It is folklore to associate an (infinite duration) two-player game with refinement, in the spirit of [3].

Definition 5 Refinement game

Let and be two models. We define a turn-based game between two players Spoiler and Duplicator (male and female, respectively) by where the set of positions V is partitioned into the positions of Spoiler and the positions of Duplicator. Since the initial position , Spoiler starts. The set of moves is the least set such that the following pairs belong to E (we take the convention that , and for convenience, we name those moves with names similar to the properties of refinement in Definition 1): Spoiler's moves Move Name whenever forth-p? whenever back-p? whenever forth-b? whenever back-b? whenever back-a? Duplicator's moves Move Name whenever forth-p! whenever back-p! whenever forth-b! whenever back-b! whenever back-a!

In the game , a play is a maximal (possibly infinite) sequence of consecutive moves, or equivalently a maximal sequence of adjacentes positions in the arena. The play is winning for Duplicator if it is infinite or if it is finite and ends in position of Spoiler, otherwise, the play ends in a position of Duplicator and it is winning for Spoiler.

A strategy of Duplicator (resp. Spoiler) is a mapping ⁎ (resp. ⁎ ) which recommends which moves to choose after each prefix of a play.

A play is an outcome of a strategy for Duplicator (resp. Spoiler) if each time Duplicator (resp. Spoiler) had to play, she (resp. he) has selected the move recommended by her (resp. his) strategy. A strategy is winning if all its outcomes are winning.

Remark 6

One easily sees that the refinement game of Definition 5 is a particular parity game [38]. Henceforth, according to [35], the refinement game is determined, and memoryless strategies suffice.

Notice that there is no forth-a move in the game , which captures the refinement relation between the structures: Lemma 7

iff Duplicator has a winning strategy in .

Proof

Assume Duplicator has a winning strategy σ in . By Remark 6 and without loss of generality, this winning σ can be taken to be memoryless. Namely, . Now, define the binary relation as the set of pairs that are reachable when Duplicator follows her strategy σ. Then it is easy to check that is an a-refinement from to . Also it is not difficult to see that if some a-refinement exists from to, then any strategy of Duplicator which maintains Spoiler's positions in , is winning. Note that by Definition 1 of a refinement, this is always possible for her.  □

We now consider a characterization of the refinement in terms of the logic . Namely, given an agent a, we define the fragment of the a-positive formulas by ◇ ◇ where and . Proposition 8

For any finitely branching (every state has only finitely many successors) pointed models and , and for any agent ,

Proof

Let us first establish that for every and , if Spoiler has a winning strategy in, then there exists a formula called a distinguishing formula for , for which but . Note that if Spoiler has a winning strategy in , all plays induced by this strategy have finite length and end in a position where Duplicator cannot move. Moreover, by a simple application of König's Lemma (as the game graph is finitely branching), the length of those plays is bounded.

We reason by induction on k, the maximal length of these plays; note that because Spoiler starts, .

If , Spoiler has a winning move from to some , where Duplicator is blocked. We reason on the form of v: • if (resp. ), then there is no move back to because (resp. ). A distinguishing formula is ¬p (resp. p).

• if (resp. ), then (resp. ). A distinguishing formula is (resp. ◇ ). The case is the same as . Since forth-a moves are not allowed in the game, position is not reachable in the game , so that the formula is not needed.

Assume now that , and pick a winning strategy of Spoiler in .

We explore the move from the initial position that is given by this strategy; because, this move cannot be either forth-p?, or back-p?. Three cases remain. forth-b? The reached position becomes , and from there Duplicator loses. That is, for each , Spoiler wins the game in at most steps. By the induction hypothesis, there exists a distinguishing formula for . It is easy to see that is a distinguishing formula for ; notice that since N is finitely branching, the conjunction is finitary.

back-b? This case applies to and to .

The reached position becomes , and from there Duplicator loses. Using a similar reasoning as for forth-b moves, it is easy to establish that there exists a formula , such that ◇

is a distinguishing formula for ; here, as M is finitely branching, a finitary disjunction is guaranteed.

Now, according to the game characterization of refinement (Lemma 7) and the determinacy of the refinement games (Remark 6), the existence of a winning strategy for Spoiler from position is equivalent to ; this provides us with the right to left direction of the proposition.

For the other direction, assume , and let with . We prove that , by induction over the structure of the formula. Basic cases where φ is either p or ¬p, but also the cases and , are immediate.

Assume . Then for every , . If, then by Property forth-b of Definition 1 this entails and consequently (whatever φ is). Otherwise, . Take an arbitrary . By Property forth-b of Definition 1, there is a with and . By induction hypothesis, , which entails .

Assume ◇ , and let be such that . By Property back-b of Definition 1, there is some , such that . By induction hypothesis, which entails ◇ .

Note that the argument still holds if we take .  □

3.3. Refinement as bisimulation plus model restriction

A bisimulation is also a refinement, but refinement allows much more semantic variation. How much more? There is a precise relation. Semantically, a refinement is a bisimulation followed by a model restriction.

An a-refinement needs to satisfy back for that agent, but not forth. Let an (‘initial’) model and a refinement of that model be given. For the sake of the exposition we assume that the initial model and the refined model are minimal, i.e., they are bisimulation contractions. Now take an arrow (a pair in the accessibility relation) in that initial model. This arrow may be missing in the refined model namely when forth is not satisfied for that arrow. On the other hand, any arrow in the refinement should be traceable to an arrow in the initial model — the back condition. There may be several arrows in the refinement that are traceable to the same arrow in the initial model, because the states in which such arrows finish may be non-bisimilar. In other words, we can see the refined model as a blowup of the initial model of which bits and pieces are cut off.

Example 9

A simple example is as follows. Consider the structure

Download full-size image and its refinement

Download full-size image by way of refinement relation . The arrow has no image in the refined model. On the other hand, the arrow has two images, namely and . These two arrows cannot be identified, because b and are non-bisimilar, and that is because there is yet another arrow from b but no other arrow from : arrow has only one image in the refined model.

The cutting off phase can be described such that the relation to restricted bisimulation becomes clear. When expanding the initial model, the blowing up phase, make a certain propositional variable false in all states of the blowup that you want to prune (that are not in the refinement relation) and make it true in all states that you want to keep. Therefore, the blown up model is bisimilar to the initial model except for the value of that variable. (In other words, it is a restricted bisimulation.) Then, remove arrows to states where that atom is false. The result is a refinement of the original model, except maybe for the value of that variable, as it is now true everywhere — in the example we have chosen a variable that was already initially true everywhere, to simplify the exposition.

Example 10

Continuing the previous example, consider the following structure bisimilar to the initial model, except for the value of atom p — in the visualization • represents that p is true and ∘ represents that p is false.

Download full-size image

The relation is a bisimulation, except for the value of p. The refinement from the previous example is a restriction of this structure, namely the result of removing the ∘ states and the arrows leading to those states.

Winding up, performing an a-refinement clearly corresponds to the following operation: Given a pointed model, first choose a bisimilar pointed model, then remove some pairs from the accessibility relation for a in that model.

Given a propositional variable q, this has the same semantic effect as Given a pointed model, first choose a bisimilar pointed model except for variable q, such that q is (only) false in some states that are accessible for a, then remove all those pairs from the accessibility relation for a.

In other words: Given a pointed model, first choose a bisimilar pointed model except for variable q, then remove all pairs from the accessibility relation for a pointing to states where q is false.

If we do this for all agents at the same time (or if we strictly regard tree unwindings of models only), we can even see the latter operation as follows: Given a pointed model, first choose a bisimilar pointed model except for variable q, then restrict the model to the states where q is true.

Of course the variable q, which has now become true everywhere, may have a value different from its value in the a-refinement. Formally, the result is as follows. First, let M be a model with accessibility relation (set of accessibility relations) R, and let be such that for all ,, then (analogously to a model restriction) is the model that is the same as M but with the accessibility restricted to . Lemma 11

Given, there is an (with accessibility function ) and some that is the same as except that , such that and .

Proof

Let an a-refinement relation be given, such that . We expand the model N and this relation as follows to a model and a bisimulation . Consider (is the set of all states in M that do not have an image in N). Now consider with domain , such that for each agent b (including a), iff: • , or

• , or

• , ,, there is a u such that , and ;

and such that on the part of the domain whereas on the new part of the domain. Now define as follows: iff or (and ). Then is a bisimulation linking and . If we restrict to , we get back (states in the part of have become unreachable). We have satisfied the proof requirement that and (for ).  □

Lemma 12

Given, there is an (with accessibility function ) and some such that and , where is the same as except that iff .

Proof

To satisfy the requirement for p, we make p false on the part of the domain of , and true on the part of the domain of . (We do not change the value of other propositional letters on .)  □

Below, is the restriction of M to the set of states satisfying p. Proposition 13

Given, there is an and some such that and is identical to except for maybe the value of p.

Proof

Clearly, in Lemma 12, . The model restriction gets rid of the part of , so we now have that is identical to (and not merely bisimilar to) except for maybe the value of p.  □

In Section 4.3 we build upon this semantic result by translating the logic with refinement quantifiers into the logic with bisimulation quantifiers plus relativization of formulas.

3.4. Refinement and action models

We recall another important result connecting structural refinement to action model execution [9]. For full details, see [55]. An action model is like a model but with the valuation replaced by a precondition function (for a given language ). The elements of are called action points. A restricted modal product consists of pairs such that, the product of accessibility relations namely such that iff and , and keeping the valuation of the state in the pair: iff . A pointed action model is an epistemic action. Proposition 14

(See [55, Prop. 4, 5].) The result of executing an epistemic action in a pointed model is a refinement of that model. Dually, for every refinement of a finite pointed model there is an epistemic action such that the result of its execution in that pointed model is a model bisimilar to the refinement.

It is instructive to outline the proof of these results.

Given pointed model and epistemic action, the resulting is a refinement of by way the relation consisting of all pairs such that . Some states of the original model may get lost in the modal product, namely if there is no action whose precondition can be executed there. But all ‘surviving’ (state,action)-pairs simply can be traced back to their first argument: clearly a refinement.

For the other direction, construct an epistemic action that is isomorphic to a given refinement of a model , but wherein valuations (determining the value of propositional variables) in states are replaced by preconditions for action execution of the corresponding action points (also called) t. Precondition should be satisfied in exactly those states such that , where is the refinement relation linking and . Now in a finite model, we can single out states (up to bisimilarity) by a distinguishing formula [13]. One then shows that can be bisimulation-contracted to . It is unknown if the finiteness restriction can be lifted, because the existence of distinguishing formulas plays a crucial part in the proof.

Example 4.2 presents an action model and its execution in an initial information state, and we will there continue our reflections on the comparison of the frameworks.

3.5. Modal specifications refinement

Modal specifications are classic, convenient, and expressive mathematical objects that represent interfaces of component-based systems [36], [44], [45], [46], [4], [49]. Modal specifications are deterministic automata equipped with transitions of two types: may and must. The components that implement such interfaces are deterministic automata; an alternative language-based semantics can therefore be considered, as presented in [44], [45]. Informally, a must-transition is available in every component that implements the modal specification, while a may-transition need not be. Modal specifications are interpreted as logical specifications matching the conjunctive ν-calculus fragment of the μ-calculus [20]. In order to abstract from a particular implementation, an entire theory of modal specifications has been developed, which relies on a refinement preorder, known as modal refinement. However, although its definition is close to our definition of refinement, the two notions are incomparable: there is no way to interpret may and must as different agents (agent a and another agent have clearly independent roles in the semantics of a-refinement), because ‘must’ is a subtype of ‘may’.

4. Refinement Modal Logic

In this section we present the refinement modal logic, wherein we add a modal operator that we call a refinement quantifier to the language of multi-agent modal logic, or to the language of the modal μ-calculus. From prior publications [55], [56] refinement modal logic is known as ‘future event logic’. In that interpretation different operators stand for different epistemic operators (each describing what an agent knows), and refinement modal logic is then able express what informative events are consistent with a given information state. However, here we take a more general stance.

We list some relevant validities and semantic properties, and also relate the logic to well-known logical frameworks such as bisimulation quantified modal logic (by way of relativization), and dynamic epistemic logics.

4.1. Syntax and semantics of refinement modal logic

The syntax and the semantics of refinement modal logic are as follows. Definition 15 Languages

Given a finite set of agents A and a countable set of propositional atoms P, the language of refinement modal logic is inductively defined as where and . Similarly, the language of refinement μ-calculus has an extra inductive clause , where X is the set of variables and .

We write for . For a subset of agents we introduce the abbreviation for (in any order), where we write ∃φ for , and similarly for and ∀. (So in the single-agent version we are also entitled to write ∀ and ∃.)

Note the two differences between bisimulation quantifiers and the refinement quantifier ∀. The former we write with a ‘tilde’-symbol over the quantifier. The latter (and also ) has no variable. A refinement quantifier can be seen as implicitly quantifying over a variable, namely over a variable that does not occur in the formula φ that it binds (nor should it occur in a formula of which ∃φ is a subformula). Section 4.3 will relate bisimulation quantification to the refinement operator.

Definition 16 Semantics of refinement

Assume a model . The set of validities of is the logic (refinement modal logic) and the set of validities of is the logic (refinement μ-calculus).

In other words, is true in a pointed model iff φ is true in all its a-refinements. Typical model operations that produce an a-refinement are: blowing up the model (to a bisimilar model) such as adding copies that are indistinguishable from the current model and one another, and removing pairs of the accessibility relation for the agent a (or, alternatively worded: removing states accessible only by agent a). In the final part of this section we relate these semantics to the well-known frameworks action model logic and bisimulation quantified logic (and see also [55]).

Proposition 17 Bisimulation invariance

Refinement modal logic and refinement μ-calculus are bisimulation invariant.

Proof

Bisimulation invariance is the following property: given and a formula φ, then iff . If the logic has operators beyond the standard modalities, this property does not automatically follow from bisimilarity.

For refinement modal logic bisimulation invariance is straightforward, noting that is bisimulation invariant, and that μx is bisimulation invariant. The new operator is bisimulation invariant, because a-refinement is transitive and bisimulation is just a specific type of a-refinement. Formally, let , and , we have to prove that . Let be arbitrary such that . From follows . From and follows by Proposition 2 that . From and follows . As was arbitrary, we therefore conclude . The reverse direction is symmetric.  □

The following result justifies our notation for sets of agents. Proposition 18

For all agents , .

Proof

Let be given and let and be such that and . We have that iff iff . (See Proposition 3.)  □

Proposition 19

The following are validities of . 1.

(reflexivity)

2.

(transitivity)

3.

(Church–Rosser)

4.

and

5. ◇ ◇

Proof

Note that the first three items directly follow from Proposition 2. 1. The trivial refinement is a refinement.

2. Composition of two refinements is a refinement.

3. Refinement satisfies the Church–Rosser property.

4. This follows from the semantics. Consider the diamond form of the equivalence. The right-to-left direction is trivial. For the left-to-right direction note that if is true in some refinement of a given model, then φ is true or ψ is true in that refinement, so is true or is true in the given model.

5. From left to right: let be such that ◇ , and let and be such that , ◇ , and . Because of back, there is a such that . Therefore and thus ◇ .

From right to left: let be such that ◇ , and let and be such that , , and . Consider the model N with point s that is the disjoint union of M and except that: all outgoing a-arrows from s in M are removed (all pairs ), a new a-arrow links s to in (add to the new ). Then is an a-refinement of that, obviously, satisfies ◇ , so satisfies ◇ . (This construction is typical for refinement modal logic semantics. It will reappear in various more complex forms later, e.g., in the soundness proof of the axiomatization RML.)

 □

The semantics of refinement modal logic is with respect to the class of all models (for a given set of agents and atoms). If we restrict the semantics to a specific model class only, we get a very different logic. For example is a validity in : just remove all access. But in refinement epistemic logic, interpreted on models, this is not a validity: seriality of models must be preserved in every refinement. See [56], [27].

4.2. Examples

Change of knowledge Given are two agents that are uncertain about the value of a fact p, and where this is common knowledge, and where p is true. Both accessibility relations are equivalence relations, so the epistemic operators model the agents' knowledge. An informative event is possible after which a knows that p but b does not know that; this is expressed by

In Fig. 2, the initial state of information is on the left, and its refinement validating the postcondition is on the right. In the visualization the actual states are underlined. If states are accessible for both a and b we have labelled the (single) arrow with ab.

Download full-size image Fig. 2. An example of refinement as change of knowledge.

On the left, the formula is true, because is true on the right. On the right, in the actual state there is no alternative for agent a (only the actual state itself is considered possible by a), so is true, whereas agent b also considers another state possible, wherein agent a considers it possible that p is false. Therefore, is also true in the actual state on the right.

The model on the right in the figure is neither an a-refinement of the model on the left, nor a b-refinement of it, but an -refinement.

Recalling Section 3.4 on action models, a refinement of a pointed model can also be obtained by executing an epistemic action (Proposition 14). Therefore, we should be able to see the refinement in this example as produced by an epistemic action. This is indeed the case. The epistemic action consists of two action points and, they can be distinguished by agent a but not by agent b. What really happens is ; it has precondition p. Agent b cannot distinguish this from with precondition ⊤.

The execution of this action is depicted in Fig. 3. The point of the structure is the one with precondition p: in fact, a is learning that p, but b is uncertain between that action and the ‘trivial’ action wherein nothing is learnt. The trivial action has precondition ⊤. It can be executed in both states of the initial model. The actual action can only be executed in the state where p is true. Therefore, the resulting structure is the refinement with three states.

Download full-size image Fig. 3. The refinement in Example 4.2.

Action models can also be added as primitives to the multi-agent modal logical language and are then interpreted with a dynamic modal operator — similar to automata-PDL. To get a well-defined logical language, the set of action model frames needs to be enumerable, and therefore such action models must be finite. Thus we get action model logic. We now recall the result in Proposition 14 that on finite models every refinement corresponds to the execution of an action model and vice versa (where the action model constructed from a given refinement may be infinite), but that it is unknown if that finiteness restriction can be lifted. If that result can be generalized, that would be of interest, as that would suggest that refinement modal logic is equally expressive as action model logic with quantification over action models. If these logics were equally expressive, action model logic with quantification would be decidable — a surprising fact, given that public announcement logic with quantification over public announcements (singleton action models) is undecidable [23].

Software verification and design Consider a class of discrete-event systems, whose elements represent devices that interact with an environment. Each device is described by means of actions c and u, respectively called ‘controllable’ and ‘uncontrollable’ actions. Given an expected property described by some formula φ, say in , we use refinement quantifiers to express several classic verification/synthesis problems. In this example, we let □φ stand for .

The the control problem [48], known as the question “is there a way to control actions c of the system S so that property φ is guaranteed?”, can be expressed in by wondering whether

The module checking problem [33] is the problem of determining whether an open system satisfies a given property. In other words, whether the property holds when the system is composed with an arbitrary environment. Let us say that action c is an abstract action that denotes internal ones, while action u abstracts all external actions, i.e. actions performed by the environment. Also, assume there is an atomic proposition e that distinguishes states where it is the turn of the system to act (thus only action c is available) from states where it is the turn of the environment (thus only action u is available). In this setting, we answer positively to the module checking problem iff . As arbitrary environments are too permissive, we may force hypotheses such as restricting to non-blocking environments: the property can be captured by the -formula ◇ , which formally says that it is always the case () that whenever in an environment state, there is an outgoing transition from that state ( ◇ ). Now, by ‘guarding’ the universal quantification over all u-refinements (i.e. all environments) with the NonBlockingEnv assumption, the statement becomes

The generalized control problem is the combination of the two previous problems, by questioning the existence of a control such that the controlled system satisfies the property in all possible environments. This is expressed by wondering whether

A last example is borrowed from protocol synthesis problems. Consider a specification, MUTEX, of a mutual exclusion protocol involving processes , and some property φ specified in . Now we may ask if we can find a refinement of MUTEX that satisfies φ but also such that if process i is in the critical section () at time, then this is known at time n. This is expressed as ◇ where AG is the CTL-modality, which is defined in as , and means that this is true at any time. The refinement consists in moving the nondeterministic choices forward, so that a fork at time n becomes a fork at time with each branch having a single successor at time n, as depicted in Fig. 4.

Download full-size image Fig. 4. The refinement of MUTEX.

4.3. Refinement quantification is bisimulation quantification plus relativization

In Section 3.3 we presented a semantic perspective of refinement as bisimulation followed by model restriction, or, alternatively and equivalently, as a restricted bisimulation, namely except for some propositional variable, followed by a model restriction to that variable. We now lift this result to a corresponding syntactic, logical, perspective of the refinement quantifier as a bisimulation quantifier followed by relativization.

More precisely, in this section we will show that a refinement formula is equivalent to a bisimulation quantification over a variable not occurring in φ, followed by a (non-standard) relativization for that agent to that variable, for which we write (to be defined shortly). For refinement ⪰ for the set of all agents (recall that we write ⪰ for , and ∃ for ) we can expand this perspective to even more familiar ground: a refinement formula ∃φ is equivalent to a bisimulation quantification over a variable not in φ followed by (standard) relativization to that variable: . These results immediately clarify in what sense the refinement modality constitutes ‘implicit’ quantification, namely over a variable not occurring in the formula bound by it.

For the syntactic correspondence we first introduce the notion of relativization (for settings in modal logic, see [53], [39]). We propose a definition of relativization that may be considered non-standard for several reasons. Firstly, it is relativization not merely to a propositional variable but also for a given agent only. The standard definition is then the special case of relativization to that variable for all agents (we will prove that consecutive relativization to the same variable for two different agents is commutative, in other words, order independent). Secondly, the relativization that we propose corresponds in the semantics to arrow elimination and not to state elimination (in other words, it does not correspond to submodel restriction). From the modal logical literature, the approach in [39] is arrow-eliminating but that in [53] is state-eliminating.

The arrow-eliminating relativization need only be done in accessible states but not in the actual state (e.g., the relativization of a variable q to a variable p is that same variable q and not ).

The difference between state-eliminating relativization and arrow-eliminating relativization is similar to the difference between state-eliminating public announcement semantics [43], [9] and arrow-eliminating public announcement semantics [32], [24], in the area of dynamic epistemic logic. As our relativization is with respect to a given agent, we have no option but to use arrow-eliminating relativization.

Given our purpose to translate refinement modal logic into bisimulation quantified modal logic, we also expand the definition of relativization to include quantifiers. This definition will then be used in Section 6. Definition 20 Relativization

Relativization to propositional variable p for agent is defined as follows.

Lemma 21

Let be a model with accessibility function R and such that: iff . Then if and only if .

Proof

The proof is by induction on the structure of φ. •

• The clauses for negation and conjunction are elementary.

•

for all

for all

for all

•

for all

for all

for all

• For a more natural argument we take the existential quantifier instead of the universal quantifier. First, observe that:

there is an

there is an

We also have that, by definition:

there is an

It remains to show that the two final statements in these chains of equivalences are also equivalent.

From left to right is easy. If, then also . In N and M we remove all a-arrows to ¬p states; and if it is already a bisimulation, then the forth and back requirements still hold for fewer pairs in the accessibility relation for a. So we can take .

From right to left is not easy. Let us first explain this informally. Given that, the part of M that is inaccessible from (i.e., not in the s-generated submodel) may not be bisimilar to anything in . This is problematic, because we need to transform to some in a way that establishes a q restricted bisimulation between and all of . Fortunately, the transformation can be an extension of , wherein we uniformly treat states in that inaccessible part of M and other states of M: we do not need to be economic in our construction. These are the details.

Let be the restricted bisimulation. To be explicit, let and let . Consider . For each we need an exact copy of M (let ) in our construction. We now define as follows: –

– for all , ;

–

and ;

– for all , .

Now take , and let as before be restriction of to pairs such that satisfies p. It is now immediate that and therefore also .

• The other clause for the universal quantifier starts with a renaming operation (that equally applies to the existential quantifier), and then proceeds as in the previous clause.

 □

Agent relativization relates as expected to the standard notion of relativization (for the set of all agents simultaneously). This is because relativization to different variables for different agents is commutative. Lemma 22

Let . Then .

Proof

By induction on the structure of φ. The non-trivial cases are , (follows dually), , and (also follows dually). Note that -relativization distributes over implication. •

•

(or else, yet another step)

 □

Given Lemma 22, we may view a nesting of relativizations as a relativization for the set of agents . Furthermore, for we can write : the usual relativization for all agents simultaneously.

To make the syntactic correspondence we now introduce a translation. Definition 23

The translation is defined by induction on . All clauses except are trivial.

Example 24

Proposition 25

Let . Then φ is equivalent to .

Proof

In the proposition we allowed ourselves a slight abuse of language: it means that, given any, the value of φ in the semantics for refinement modal logic is equivalent to the value of in the semantics for bisimulation quantified modal logic. The proposition follows from Lemma 12, Lemma 21 and Definition 23. We show the case of the inductive proof — and to suit the intuition we take the existential quantifier .

iff

there is an such that and

iff (I.H.)

there is an such that and

iff (Lemma 12)

there is an with (restr. to p true) s.t. and

iff (Lemma 21)

there is an such that and

iff

iff

.  □

This corollary makes the characteristic cases of Proposition 25 stand out. Corollary 26

Consider ∃φ with (i.e., ∃-free). Then • a-refinement is bisimulation quantification plus a-relativization:

is equivalent to ;

• refinement is bisimulation quantification plus relativization:

∃φ is equivalent to .

In the logic of public announcements, the latter is written as: ∃φ is equivalent to .

4.4. Alternating refinement relations

Alternating transition systems (ATS) were introduced [3] to model multi-agent systems, where in each move of the game between the agents of an ATS, the choice of an agent at a state is a set of states and the successor state is determined by considering the intersection of the choices made by all agents. A notion of a-alternating refinement was introduced to reflect a refined behavior of agent a while keeping intact the behavior of the others. When restricting to turn-based ATS where only one agent plays at a time (concurrent moves are also allowed in the full setting), a-alternating refinement amounts to requiring ‘forth’ for all as we do, but ‘back’ just for agent a. As a consequence, an a-refinement is a particular a-alternating refinement. A logical characterization of a-alternating refinement has been proposed (it essentially relies on the modality combined with the linear time temporal logic LTL) in the sense that if an ATS a-refines an ATS , every formula true in is also true in . Notice however that the operator has a more restricted semantics than the one we propose, since the quantification does not range over all possible refinements of the structure but only over refinements obtained by pruning the unraveling of the ATS. Soon after, the more general setting of alternating-time temporal logics [2] considered universal and existential quantifications over a-refinements, for arbitrary a, combined with LTL formulas. It is worthwhile noticing that the quantifiers still range over particular refinements, and always in the original structure. As a consequence, the language cannot express the ability to nest refinements for different agents. This is easily done in our language , as the formula ◇

exemplifies. This formula tells us that one of the choices that a can make, results in b knowing p and a contemplating a subsequent choice by b that makes her to get to know p as well.

5. Axiomatization RML

Here we present the axiomatization RML for the logic . We show the axioms and rules to be sound, we give example derivations, and this is followed by the completeness proof.

The axiomatization presented is a substitution schema, since the substitution rule is not valid. The substitution rule says that: if φ is a theorem, and p occurs in φ, and ψ is any formula, then is a theorem. Note that for all atomic propositions p, is valid, but the same is not true for an arbitrary formula, e.g. ◇ ◇

is not valid, because after the maximal refinement there is no accessible state, so that

◇

is then false even if it was true before. The logic  is therefore not a normal modal logic.

Definition 27 Axiomatization RML

The axiomatization RML consists of all substitution instances of the axioms ◇ and the rules where , , and . If φ is derivable, we write ⊢φ, and φ is called a theorem, as usual. The well-known axiomatization K for the logic consists of the axioms Prop, K, and the rules MP and NecK.

In the definition, given , note that ◇

stands for

◇

(see the technical preliminaries) and so for

◇ ◇ . The axiomatization RML is surprisingly simple given the complexity of the semantic definition of the refinement operator ∀; and given the well-known complexity of axiomatizations for logics involving bisimulation quantifiers instead of this single refinement quantifier. We note that while refinement is reflexive, transitive and satisfies the Church–Rosser property (Proposition 2, and Proposition 19), the corresponding modal axioms are not required. These properties are schematically derivable. First, we demonstrate soundness of RML. Given the definitions of □ and ◇ in terms of cover, it may be instructive to see how the RK axiom works as a reduction principle for and ◇

— note that we need both, as there is no principle for . For simplicity we do not label the operators with agents. We get (for the second equivalence, see also Proposition 33, later):

◇ and ◇ ◇ ◇ ◇ One may wonder why we did not choose and ◇ ◇

(we recall Proposition 19) as primitives in the axiomatization, as, after all, these are very simple axioms. They are of course valid, but the axiomatization would not be complete. The axiom RK is much more powerful, as this not merely allows , , and , but any finite set of formulas.

5.1. Soundness

Theorem 28

The axiomatization RML is sound for .

Proof

As all models of are models of, the schemas Prop, K and the rule MP and NecK are all sound. We deal with the remaining schemas and rules below.

R

Suppose that is a model such that , and . Then for every , where , we have , and also . From and follows . As was arbitrary model such that , from that and follows .

RProp

Let and be given such that . By Definition 1 for the semantics of refinement, we have that if and only if . Therefore iff , for every and with . Therefore iff for every , i.e. . Similarly, for , using that if and only if .

RK

Suppose is a model, where , such that for some set Φ, . Therefore, there is a model such that — where . Expanding the definition, we have that for every there is some such that . Also, because of back, for every such there is some such that . Combining these statements we have that for every there is some such that , and thus ◇ .

Conversely, suppose that ◇ . Therefore, for every there is some such that . Thus, for each, there is some model , where , such that . Without loss of generality, we may assume that for all the models and are disjoint.

We construct the model such that: where if and else .

We can see that , via the relation where is the identity on S and each is the refinement relation corresponding to (see also [25]). Furthermore, for each it is clear that for some φ, and thus , and so . Therefore . Finally, for each there is some where , so for each we have ◇ , so we have ◇ . Combined, and ◇

state that , and therefore .

RKmulti

Suppose that . Therefore, there is a model such that — let the accessibility relation for agent b in be . Expanding the definition, we have that for every there is some such that . Also, because of back, for every such there is some such that . Combining these statements we have that for every there is some such that , and thus ◇ . However, as forth also holds for agent b, the we could construct above are also all the states v accessible from s. Therefore we also have , so together we get .

For the converse direction, suppose that . From the definition of it follows that ◇ . We now proceed in a similar way as in the case RK. From ◇

it follows that for every  there is some  such that . Thus, for each, there is some model , where , such that . Define the model  similar to the case RK, except that: the roles of a and b have been swapped, and the accessibility relation for all agents c different from a and b is defined as that for a.

where if and else (also defines , namely for ).

We can see that , via the relation where is the identity on S and each is the refinement relation corresponding to (see also [25]). Furthermore, for each it is clear that for some φ, and thus , and so . Therefore . Finally, for each there is some where , so for each we have ◇ , so we have ◇ . Combined, and ◇

state that , and therefore .

RKconj

The direction is merely a more complex form of pattern which is derivable similar to ◇ ◇ ◇

in the modal logic , using the axiom R in place of K.

For the other direction, suppose that is such that , where . We need to show that . To do this we follow the same strategy as for proving RK: we construct an a-refinement of , and show that .

We begin by constructing the model . Suppose that . Then we have , and by RK this implies that ◇ . We also have that for every , , and by RKmulti this implies that , and by the definition of the cover operator, this implies that ◇ . Hence for every and , we have that ◇ . (In other words, for some big set of formulas Ψ we have that ◇ .) At this stage it suffices to refer to the very similar construction in the soundness proof for axiom RK, from which, similarly to there, it follows that .

NecR

If φ is a validity, then it is satisfied by every model, so for any model , φ is satisfied by every model , and hence every model satisfies .  □

The soundness of axiom RK is visualized in Fig. 5. It depicts the interaction between refinement and modality involved in this axiom ◇ , for the case that . The single lines are modal accessibility, and the double lines the refinement relations. The solid lines are given, and the dashed lines are required. Accessibility relations for other agents than a are omitted. The picture on the left depicts the implication from left to right in the axiom, and the picture on the right depicts the implication from right to left. Note that the states satisfying and have the same origin u in M — the typical sort of duplication (resulting in non-bisimilar states) allowed when having back but not forth. Apart from u and t, state s in M has yet another accessible state v, that does not occur in the refinement relation: the other typical sort of thing when having back but not forth. Therefore, on the right side of the equivalence in axiom RK we only have ◇

and we cannot guarantee that  also follows from the left-hand side.

Download full-size image Fig. 5. The interaction between refinement and modality involved in axiom RK.

The axiom RKmulti, defined as for , says that refinement with respect to one agent does not interact with the modalities (the uncertainty, say) for another agent: the operators and simply commute. This in contrast to the axiom RK where on the right-hand side a construct is ‘missing’, so to speak. If it had been ◇ , then we would have had , as in RKmulti but with .

The axioms RK and RKmulti are different, because in an a-refinement the condition forth is not required, whereas for other agents b forth is required. Given some refinement wherein we have a cover of Φ, so that at least one of Φ is necessary (the bit), for each of the covered states we can trace an origin before the refinement, because of back. But there may be more originally accessible states, so whatever holds in those origins, although it is all possible, is not necessary. So we have ◇ , but we do not have . In contrast, when the agents are different, back and forth must hold for agent b in a refinement witnessing the operator : for an a-refinement, back and forth must hold for all agents . Fig. 6 should further clarify the issue — compare this to Fig. 5. The main difference between the figures is that there cannot now be yet another state v accessible from s but not ‘covered’ as the origin of one of the refined states. In Fig. 5 what holds in t and u is not necessary for a, but in Fig. 6 what holds in t and u is necessary for b.

Download full-size image Fig. 6. The interaction between refinement and modality involved in axiom RKmulti.

5.2. Example derivations

In these examples we also use ‘substitution of equivalents’, see Proposition 32, ahead.

Example 29

◇ ◇ .

In an epistemic setting, where means that the agent knows p, and where (in S5 models) the condition ◇

is always satisfied, this validity expresses that the agent can always find out the truth about p: if true, announce p to the agent (and announcement is a model restriction, and therefore a refinement), after which p is known by the agent to be true, and if false, announce that p is false, after which p is known to be false. This validity is indeed also a theorem of . For that, it suffices to derive the equivalent

◇ . In some cases several deductions have been combined into single statements, but this is restricted to cases of well-known modal theorems. ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ Lines 3 and 4 of the derivation require the following derivation, where φ is a propositional formula (i.e., ). ◇ ◇ ◇

Example 30

◇ ◇ ◇ ◇ .

Consider the informative development described in Example 4.2: given an initial information state wherein agents a and b consider either value of p possible, a can be informed such that afterwards a believes that p but not b. This theorem formalizes that. In the following, let φ be ◇ ◇ ◇ ◇ . ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇

5.3. Completeness

Completeness is shown by a fairly but not altogether straightforward reduction argument: every formula in refinement modal logic is equivalent to a formula in modal logic. So it is a theorem, if its modal logical equivalent is a theorem. In the axiomatization RML we can observe that all axioms involving refinement operators ∃ are equivalences, except for R; however, is a derivable theorem. This means that by so-called ‘rewriting’ we can push the ∃ operators further inward into a formula, until we reach some expression ∃φ where φ contains no refinement operators. Now we come to the less straightforward part. Because there is a hitch: there is no general way to push a ∃ beyond a negation (or, for that matter, beyond a conjunction). For that, we use another trick, namely that all modal logical formulas are equivalent to formulas in the cover logic syntax, and that all those are equivalent to formulas in disjunctive form (see the introduction) in cover logic. Using that, once we reached some innermost ∃φ where φ contains no refinement operators, we can continue pushing that refinement operator downward until it binds a propositional formula only, and disappears in smoke because of the RProp axiom. Then, iterate this. All ∃ operators have disappeared in smoke. We have a formula in modal logic.

For a smooth argument we first give some general results, after which we apply the reduction argument and demonstrate completeness.

Definition 31 Substitution of equivalents

An axiomatization satisfies substitution of equivalents if the following holds. Let and . If then .

Proposition 32

The axiomatization RML satisfies substitution of equivalents.

Proof

This can be shown by induction on . All cases are standard. The case is shown by using an inductive hypothesis and then successively applying NecK, K, and some elementary tautologies and applications of MP. (The required pattern is: from , to , to . Then, similarly, for the other direction of the equivalence . Then, some more propositional steps to wind it up.) Whereas the case is shown with the same inductive hypothesis but applying NecR and R instead of NecK and K.  □

Proposition 33

1. .

2. .

3. .

Proof

Item 1. can be easily derived from R, NecR and MP, similarly to the way that in modal logic we derive . Item 2. is the dual of item 1. and requires mere propositional reasoning. Item 3. can be derived using the tautologies and , respectively, propositional reasoning, and R. (Alternatively, for Item 3., we can think of deriving its dual, with the crucial steps in the derivation that is a tautology, from which with R and MP we get .)  □

Proposition 34

1.

for all propositional φ.

2.

for all propositional φ.

Proof

We show for all propositional φ. The proof of for all propositional φ is similar. For convenience in the proof we omit the agent label and write ∀.

We first show . Assume that φ is in disjunctive normal form (i.e., for propositional logic, different from the disjunctive form, df, often used in this work). Formula φ therefore has the form , where each formula γ is a conjunction of atoms or their negation, for which we write, slightly abusing the language, — where if p is a conjunct of γ and if ¬p is a conjunct of γ. We now get the following. We omit trivial steps of chaining implications and applying MP. For readability we assume the ‘φ→’ part in some derived formulas.

For the converse direction we convert φ to the conjunctive normal form for propositional formulas, i.e., φ is equivalent to (where we now write if p is a disjunct — not conjunct — of γ and if ¬p is a disjunct of γ). ⁎ We show why * holds by outlining the method and giving an example: write the conjunct in implicative fashion, e.g., instead of we write . Then, applying NecR and R and MP repeatedly, we get first and then . Then, applying RProp, we get , in other words, we have back.  □

Proposition 35

for all propositional φ (and any ).

Proof

Proposition 33 demonstrated that from which, using Proposition 34.2, also follows . For the other direction we first derive by propositional means and applications of Nec and R. This goes as follows. For convenience of applying the available axioms, instead of use the equivalent form . Now we observe that is a tautology and therefore derivable, applying NecR gets us and successively applying R gets us . Then, finally, we use that (Proposition 34.1) and thus get .  □

We now first show that every formula is logically equivalent to an formula. We then show that if the latter is a theorem in K, the former is a theorem in RML.

Proposition 36

Every formula of is logically equivalent to a formula of .

Proof

Given a formula , we prove by induction on the number of the occurrences of in ψ (for any ) that it is equivalent to an -free formula, and therefore to a formula, the standard modal logic. The base is trivial. Now assume ψ contains occurrences of -operators for some (so these may be refinement operators for different agents). Choose a subformula of type of our given formula ψ, where φ is -free for any (i.e. choose an innermost ). Let be a disjunctive formula that is equivalent to φ. We prove by induction on the structure of that is logically equivalent to a formula χ without . There are two cases: •

•  where is propositional, , and each a set of dfs.

In the first case, apply Proposition 33.2, we get , and then apply induction. In the second case, if we use that (Proposition 34.2). If, then from Proposition 35 follows that this is equivalent to , and we further reduce the right conjunct with one of the axioms RK (if ), RKmulti (if with ), or RKconj (if ), and apply induction again.

Thus we are able to push the refinement operators deeper into the formula until they eventually reach a propositional formula, at which point they disappear and we are left with the required ∃-free formula χ that is equivalent to ∃φ. Replacing by χ in ψ gives a result with one less ∃-operator, to which the (original) induction hypothesis applies.  □

Proposition 37

Let be given and be equivalent to φ. If ψ is a theorem in K, then φ is a theorem in RML.

Proof

Given a , Proposition 36 gives us an equivalent . Assume that ψ is a theorem in K. We can extend the derivation of ψ to a derivation of φ by observing that all steps used in Proposition 36 are not merely logical but also provable equivalences — where we also apply Proposition 32 of substitution of equivalents.  □

Theorem 38

The axiom schema RML is sound and complete for the logic .

Proof

The soundness proof is given in Theorem 28, so we are left to show completeness. Suppose that is valid: ⊨φ. Applying Lemma 36 we know that there is some equivalent formula , i.e., not containing any refinement operator. As φ is valid, from that and the validity it follows that ψ is also valid in refinement modal logic, and therefore also valid in the logic K (note that the model class is the same). From the completeness of K it follows that ψ is derivable, i.e. it is a theorem. From Proposition 37 it follows that φ is a theorem.  □

5.4. The single-agent case

The axiomatization for the single-agent case is the unlabelled version of RML, minus the axioms RKmulti and RKconj. The single-agent axiomatization was presented in [56]. The completeness proof there is (slightly) different from the multi-agent case of the proof here. In [56] it is used that every refinement modal logical formula is equivalent to a formula in cover logic with the special syntax [10], [34], plus induction on that form. (This syntax is of course very ‘disjunctive formula like’.) That proof was suggested by Yde Venema, as a shorter alternative to the proof with disjunctive forms.

5.5. Refinement epistemic logic

Refinement modal logic is presented with respect to the class of all models. As mentioned in Section 4.1, by restricting the class of models that the logic is interpreted over, we may associate different meanings with the modalities. For example, the epistemic logic S5, a.k.a. the logic of knowledge, is interpreted over the model class , and the logic of belief KD45 is interpreted over the class . Given any class of models, the semantic interpretation of ∀ is given by: Thus we can consider various refinement epistemic logics. Although is a validity in (just remove all access) it is not so in the refinement logic of knowledge, interpreted on models, because seriality of models must be preserved in every refinement. And therefore it is also not valid in the refinement logic of belief.

Our axiomatization RML may not be sound for more restricted model classes. Let us consider the single-agent case, and the axiom ◇ For example, in we have that is inconsistent, but that ◇ ◇

is consistent: you do not consider an informative development possible after which you both know and don't know p at the same time. Therefore, axiom RK is invalid for that class.

The axioms replacing RK in refinement logic of knowledge and refinement logic of belief are, respectively: ◇ and, for , ◇ where Φ is a set of purely propositional formulas. Now if apart from RS5 we also add the usual S5 axioms T, 4, and 5, we have a complete axiomatization for the refinement logic of knowledge. In the case of the refinement logic of belief, we add axioms D (for seriality), 4, and 5 and RKD45 to get a complete axiomatization. For details, see [27].

A study of how various classes of models affect the properties of bisimulation quantified logics is given in [22]. Refinement epistemic logics are investigated in [27], [25]. In [25] a multi-agent axiomatization is also reported. (For multi-agent S5, see ‘Recent results’ in Section 8.)

6. Axiomatization

In this section we give the axiomatization for refinement modal μ-calculus. We restrict ourselves to single-agent refinement modal μ-calculus. The axiomatization is an extension of the (single-agent) axiomatization RML for refinement modal logic.

We recall the definition of modal μ-calculus in the technical introductory Section 2. In [22, Lemma 2.43] a bisimulation quantifier characterization of fixed points is given. The characterization employs the universal modality ■ which quantifies over all states in the model. Let be the language of bisimulation quantified modal logic with ■ as well. First, observe that this impacts the semantics of bisimulation quantification. For two models to be bisimilar, it must now also be the case that every state in one model is bisimilar to a state in the other.

We can inductively define a truth-preserving translation . The crucial clauses are those for the fixed-point operators. The atoms p introduced in the translation are required not to occur in φ. The first equation captures the intuition of a greatest fixed point as a least upper bound of the set of states that are postfixed points of φ, whereas the second equation captures a least fixed point as the greatest lower bound of the set of states that are prefixed points of φ. From [15] we know that bisimulation quantifiers are also expressible in the modal μ-calculus, and thus these equivalences also hold in the modal μ-calculus.

Having these tools for modal μ-calculus at our disposal, let us now apply them in refinement modal μ-calculus. In order to demonstrate the soundness of the axiomatization defined below, we need to expand the relativization (Definition 20), single-agent version, to a version by including a clause for the universal modality: Employing that expanded relativization we can expand the translation (Definition 23) to a translation by adding the two clauses above for fixed points (this explains why we also wrote there). This translation t remains truth-preserving (due to Proposition 25 and [22, Lemma 2.43]). We recall the crucial interaction of the translation and the relativization, namely that is equivalent to . The translation plays an important role in the soundness proof: axioms are shown to be sound by showing that their translations are valid.

Definition 39 Axiomatization

The axiomatization is a substitution schema of the (single-agent) axioms and rules of RML along with the axiom and rule for the modal μ-calculus: and two new interaction axioms:

For single-agent RML, see Definition 27 and Section 5.4. We recall that single-agent RML does not contain the axioms RKmulti and RKconj.

We emphasize that the interaction axioms have the important associated condition that the refinement quantification will only commute with a fixed-point operator if the fixed-point formula is a disjunctive formula.

6.1. Soundness

The soundness proofs of Section 5.1 still apply and the soundness of F1 and F2 are well known [5], so we are left to show that and are sound. In the proof we use the characterization of refinement quantification in terms of bisimulation quantification and relativization that was established in Proposition 25. We will also use the characterization of both fixed points in terms of bisimulation quantification as in the previous subsection. Theorem 40

The axioms and are sound.

Proof

The proof consists of two cases, and .

Case

It is more convenient in this proof to reason about the axiom in its contrapositive form: . The proof demonstrates that is equivalent to in bisimulation quantified logic (with the universal modality). Using the translation and relativization equivalences above we have that, for any : (⁎) This proof simply applies known validities of bisimulation quantifiers. Note that line (⁎) is not an equivalence. The other direction holds if φ is a df. This we now prove.

We may assume w.l.o.g. that disjunctive formula contains no free variables, i.e., φ is (also) a disjunctive formula with only the free variable x. We recall that in a disjunctive formula, a conjunction can only be between a purely propositional part and a cover modality part, and that fixed-point variables are not allowed in the propositional part (see Section 2). Importantly, this means that propositional variable q (witnessing fixed-point variable x), that occurs in the formula , can only appear in a conjunction if it appears in the scope of a cover operator within that conjunction. This has the following significant consequence: If , where φ is a disjunctive formula, then there is a model such that ⁎

where

⁎

is the restriction of  to states that are not successors of q states.

That is, whether or not satisfies is invariant to any successors of states in ⁎ .7 To see this, we note that a disjunctive formula is true at only if there is some pointed model that is bisimilar to , and some minimal relation ρ between the states of and subformulas of such that: 1.

2. if, then either or but not both;

3. if, then and for every successor of v there is a unique such that , and for every, there is at least one successor of v where ;

4. if, then , where .

It is clear that such a relation exists when . As q is replacing the fixed-point variable x, the minimality of ρ guarantees that if vρq, then there is no formula such that . To see this we consider how the formulas q and may have appeared in , and specifically what is their smallest common super-formula: if it is a disjunction, then only the disjunct containing q will be considered; and if it is a cover operator, ∇Φ, we may assume that each disjunctive formula in Φ is related to a unique successor state in N. The smallest common super-formula can not be a fixed-point formula. Consequently, if vρp the successors of v do not impact the existence of the relation ρ, and thus do not affect whether or not .

An explicit construction for can be given via the tableaux of Janin and Walukiewicz [30]. Using their tableaux [30, Def. 3.1], the concept of a marking [30, Def. 3.6] can be adapted to give the required model, . This construction is important for the proof now to follow.

Suppose is any countable model such that , where φ is a df. We would like to build some model such that • ,

•

We inductively build a sequence of (pointed) models such that , and furthermore, the models are fixed up to a given set of states.

Definition 41

Suppose that is a pointed tree-like model (so for each, there is at most one such that ). Let . The model up to T (written ) is the model where is the set of states that are not proper descendants of T and .

Effectively, the model is the model with all the successors of any state in T removed. For each i there will be a set of states such that for all , .

This means we are able to give a well-defined limit for this sequence. At each point of the induction, will represent a frontier of states in the model where we require to be true. Because we are working with disjunctive formulas, we can change the submodels rooted at states in , without affecting the interpretation of in other parts of the model. This way we are able to find a single model with the required properties.

We now define the sequence of models . For each i we define a model and a set of states on which we will extend the construction. The proposition to be shown by inductive proof is To define the base case, it is sufficient to let and . It is clear that the induction hypothesis holds here. Now, for the inductive step, assume that the proposition holds for i. For each , we have Hence, for each, there is some (tree-like) such that We will assume w.l.o.g. that all models for and have disjoint sets of states. As φ is a disjunctive formula, we may further assume that is invariant to any successors of . This allows us (as the induction proceeds) to replace the submodels rooted at without affecting whether is satisfied in other parts of the model.

We now append the models (for ) to the model . Formally, let , and . Then Finally, we let .

We can see that the proposition to be shown holds for as follows: •

since, for all , , and  from the induction hypothesis. A -bisimulation between and can be constructed by composing these bisimulations.8

• , since for all , , and .

•

by the reasoning presented above, is invariant to the successors of the states in . Therefore, if, then .

•

follows immediately from the construction.

We now let where •

iff for some i,  for all ,

•

iff for some i,  for all ,

•

iff for some i,  for all ,

and let . It is clear that the limit step will also preserve the induction hypothesis, so we have and , since by construction . Thus, (i.e., ) as required.

The construction is represented in Fig. 7.

Download full-size image Fig. 7. The inductive step for the construction of . The formula is independent of any state where p is not true, or any state beyond the frontier defined by .

Case

We also use the contrapositive form of the axiom: . For any we have that: (⁎⁎) ( ⁎ ⁎ ⁎ ) The equivalence in ( ⁎ ⁎ ⁎ ) is true because ⧫ is the existential modality which quantifies over all states in the model. Obviously, the implication in line (⁎⁎) is only true in one direction (the usual quantifier swap ).

To prove the other direction in the equivalence , we now show directly that in refinement μ-calculus, for φ a df (observe that is then a df as well). We use the inductive characterization of of [5] which tells that if and only if for some ordinal τ, where we recall the definition of the semantic operation : , and whenever , where with .

Suppose . Since is bisimulation invariant, without loss of generality we may suppose that M is a countable tree-like model. As satisfies, there must be some least ordinal τ whereby . We give a proof by induction over τ that implies . The base case where is trivial. Now consider with . Then . As is a df, there is a refinement of with a frontier such that x may only be true at s or on this frontier, and no point beyond the frontier affects the interpretation of φ. Formally, there is a set of states such that (i.e., ), where with •

is the set of states reachable from s, but not from any ;

• , for ; and

• .

We note that is a refinement of . Now as for each i, for some , by the inductive hypothesis we may assume there is some model where and . We may append these models to , to define ⁎ ⁎ ⁎ ⁎

where

⁎ , ⁎ , and ⁎

for all . (Notice the similar construction in the soundness proof of axiom RK.) It is clear that

⁎

is a refinement of , and by the axiom F1 we can see

⁎

as required.  □

The general form of is not sound. For example, take ◇ ◇ . Then is true if p is true at every immediate successor of the current state, whereas is only true at states with no successor. Likewise is not true in the general case, as can be seen by taking ◇ . Then is true if and only if p is true at every reachable state, and is true only if p is true at every state within one step.

6.2. Completeness

The completeness proof of proceeds exactly as for Theorem 38, replacing the formulas in cover logic with disjunctive formulas, to get a statement similar to that of Proposition 36.

Proposition 42

Every formula of is equivalent to a formula of .

Proof

Given a formula ψ, we prove by induction on the number of the occurrences of ∃ in ψ that it is equivalent to an ∃-free formula, and therefore to a formula in the modal μ-calculus . The base is trivial. Now assume ψ contains ∃-operators. Choose a subformula of type ∃φ of our given formula ψ, where φ is ∃-free (i.e. choose an innermost ∃). As φ is ∃-free, it is semantically equivalent to a formula in disjunctive normal form, and by the completeness of Kozen's axiom system [59] this equivalence is provable in . By NecR and R it follows that ∃φ is provably equivalent to some formula ∃ψ where ψ is a disjunctive formula (analogously to Proposition 32 one can easily show that satisfies substitution of equivalents). Thus without loss of generality, we may assume in the following that φ is in disjunctive normal form. We may now proceed by induction over the complexity of φ, and conclude that ∃φ is logically equivalent to a formula χ without ∃. All cases of this induction are as before, we only show the final two, different cases: •

iff  (by  noting that all subformulas of a disjunctive formula are themselves disjunctive); IH.

•

iff  (by ); IH.

Replacing ∃φ by χ in ψ gives a result with one less ∃-operator, to which the (original) induction hypothesis applies.  □

Theorem 43

The axiom schema is sound and complete for the logic

Proof

Soundness follows from Theorem 40 and Theorem 28. To see is complete, suppose is a valid formula. Then by Lemma 42, φ is provably equivalent to some valid formula . As ψ is valid, it must be provable since Prop, K, F1, F2, NecK, and MP give a sound and complete proof system for the modal μ-calculus [59]. A proof of φ follows by MP.  □

7. Complexity

Decidability for both and follows from the fact that a computable translation is given in the completeness proofs of Sections 5 and 6: note that the given translations to and respectively, are recursive and involve transforming formulas into their disjunctive normal forms. Hence they are non-elementary in the size of the original formula. This non-elementary procedure for is optimal as shown in Section 7.1 below.

Unfortunately we were not able to corroborate in this paper the upper complexity claims for reported in [56]. But towards some indication of a result in that direction, we further establish a doubly exponential succinctness proof for in Section 7.2. (On complexity, see also ‘Recent results’ in Section 8.)

7.1. is non-elementary

This section is dedicated to the proof of the following result.

Theorem 44

The satisfiability problem for is non-elementary, even for the single-agent setting.

In the rest of this section, we only consider a single-agent setting.

First, we recall a fragment, written , of the standard branching-time logic Computation Tree Logic () [14], which in turn is a fragment of (see also the example Section 4.2). ◇

Let M be a model and s be an M-state. A path from s is a finite or infinite sequence of states s.t. and each is a successor of . Only the semantics of and is recalled (as for other formulas it is clear):

Directly translating in is routine via the following mapping , defined by induction over the formulas: , , , , , ◇ ◇ , ◇ , .

We also use standard abbreviations for the duals iff (‘universal always’), and iff (‘existential always’). A formula is in positive form if negation is applied only to propositional variables. A formula φ is existential if it is in positive form and there are no occurrences of the universal modalities and and the modality □. The following can be proved by using Proposition 8, enriched for the case of formulas (with a transfinite induction argument for this fixed-point formula).

Proposition 45

Let and be two models with . Then for each existential formula φ, implies .

Definition 46 Refinement

Refinement (for short) is the extension of with the refinement quantifiers ∃ and ∀.

Definition 47 Refinement Quantifier Alternation Depth

We first define the alternation length of finite sequence ⁎

of quantifiers, as the number of alternations of existential and universal refinement quantifiers in χ. Formally, ,  for every

⁎ , and if , otherwise.

Given an (resp., , resp., ) formula φ, the refinement quantifier alternation depth of φ is defined via the standard tree-encoding of φ, where each node is labeled by either a modality, a boolean connective, or a propositional variable. Then, is the maximum of the alternation lengths where χ is the sequence of refinement quantifiers along a maximal path of from the root.

Theorem 48

Let the class . The satisfiability problem for is k-Expspace-hard, for any k.

Theorem 48 is proved by a polynomial-time reduction from satisfiability of Quantified Propositional Temporal Logic () [50]. First, we recall the syntax and the semantics of . The syntax of formulas φ over a countable set P of propositional variables is defined as follows: where , is the ‘next’ modality, is the ‘eventually’ modality, and is the existential quantifier.9 We also use standard abbreviation for (‘always’).

The semantics is given w.r.t. elements of , namely infinite words w over . Beforehand, we need some technical notions. Let . For each , denotes the ith symbol of w. Moreover, for each , we define the equivalence relation over : two infinite words and are -equivalent whenever their projections onto are equal. The projection of an infinite word w onto , written , is obtained by removing from each symbol of w all the propositions in . Hence, iff .

Given a formula φ, an infinite word w over , and a position along w, the satisfaction relation is inductively defined as follows (we omit the clauses for the boolean connectives):

We say that the word w satisfies φ, written , if . A formula φ is in positive normal form if it is of the form , where for each , and is a quantification-free -formula in which negation is applied only to propositional variables.10 The quantifier alternation depth of is the number of alternations of (existential and universal) quantifiers in the string . The following is a well-known result.

Theorem 49

(See [50].) Let . Then, the satisfiability problem for the class of formulas in positive normal form whose quantifier alternation depth is k is k-Expspace-hard.

Note that Theorem 49 holds even if we assume that formulas in positive normal form like (with quantification-free) are such that are pairwise distinct, each proposition occurring in is in , and .

Theorem 48 directly follows from Theorem 49 and the following theorem, whose proof is given in the rest of this section.

Theorem 50

For every , one can construct in time polynomial in the size of φ a formula , such that φ is satisfiable if, and only if, is satisfiable. Moreover, the refinement quantifier alternation depth of , , is equal to the quantifier alternation depth of φ.

Before proving Theorem 50, we need additional definitions. Let and , where , are fresh propositional variables (intuitively, is used to encode the negation of for each , and is a new variable that will be used to mark a path). For a model M and two states s and in M, is reachable from s if there is a finite path from s leading to . Let . A pointed model (over ) is well-formed w.r.t. j if the following holds: 1. for each state of M which is reachable from s, there is exactly one proposition such that (we say that is a p-state); moreover, s is a -state;

2. each state reachable from s which is not a -state has no successor;

3. each -state which is reachable from s satisfies: (i) has some -successor, (ii) for all , either has a -state successor or (exclusive) a -state successor, and (iii) for all , has both a -state successor and a -state successor.

For each, the following formula over characterizes the set of pointed models which are well-formed w.r.t. j: ◇ ◇ ◇ ◇ Intuitively, enforces the existence of infinite paths which visit only -states such that the following holds: the set of successors of ‘encodes’ a specific truth valuation of the variables and all the possible truth valuations of the variables .

A pointed model is well-formed if it is well-formed w.r.t. j for some . In this case, we say that is minimal if, additionally, each -state which is reachable from s has exactly one -successor.

A well-formed pointed model encodes a set of infinite words over , written , given by: iff there is an infinite path of M from s (note that π consists of -states) such that for all and , either and has some -successor, or and has some -successor.

Note that if is well-formed w.r.t. 0, then . If instead is well-formed w.r.t. j for some and is also minimal, then there is an infinite word such that . In particular, when , is a singleton.

Also, one can easily see that if then .

Construction of the formula (in Theorem 50) Pick a formula . For each , we let (note that corresponds to φ).

First, we construct a formula over by using the formulas , for each . The construction is based on an induction on as follows: Base case (). Recall that is a quantification-free formula in positive normal form over P. Let ϒ be the following mapping from the set of quantification-free formulas ξ over P in positive normal form to the set of existential formulas over (it is defined by induction). • ◇ ◇

for each ;

•

and ;

• ◇ , , and .

Then, .

Induction case (). Recall .

Then, .

Finally, the formula over is given by .

Correctness of the construction Note that the size of is polynomial in the size of φ. Moreover, the refinement quantifier alternation depth of is equal to the quantifier alternation depth of φ. Thus, in order to prove Theorem 50, it remains to show that φ is satisfiable iff is satisfiable. For this, we need three preliminary lemmata.

Lemma 51

Let be a pointed model which is well-formed w.r.t. n and minimal, with . Then, for each quantification-free formula ξ in positive normal form, if and only if .

Proof

Let be the unique infinite path of M from state s (note that π consists of -states). Then, by a straightforward structural induction, one can show that for each quantification-free formula in positive normal form ξ, the following holds: for all , iff . Hence, the result follows. □

Let and let be a pointed model which is well-formed w.r.t. j. For each , an h-segment of is a refinement of which is well-formed w.r.t. h and minimal. Note that for each and for each , by construction, there exists an h-segment of such that .

Lemma 52

Let and be a pointed model which is well-formed w.r.t. such that for each , . Then, .

Proof

The proof is by induction on . Base case (). Recall , where is a quantification-free formula in positive normal form. By construction, . Let be a refinement of which satisfies formula (if any). We need to show that . By definition of , is well-formed w.r.t. n. Let be any n-segment of , and let . By transitivity, is a refinement of , so that . Thus, by hypothesis, , which implies . By Lemma 51, it follows that . Since is a refinement of and is an existential formula, by Proposition 45 we deduce that as well. Hence, the result holds.

Induction step (). By construction, there are two cases:

(1) and : let . By hypothesis, . Hence, there is infinite word over such that and . Since is well-formed w.r.t. and , it follows that as well. Let be any j-segment of such that . By definition of , . Thus, it suffices to show that . Since is well-formed w.r.t. j and minimal, and , it holds that for each , . Since every proposition in does not occur free in and , it follows that for each , . Thus, by the induction hypothesis, we obtain that , and the result holds.

(2) and : let be a refinement of which satisfies formula (if any). We need to show that . By definition of , is well-formed w.r.t. j. Thus, by the induction hypothesis it suffices to show that for each , . Let . Since is a refinement of , it holds that . Thus, by hypothesis, . Hence, , and the result follows.

 □

Lemma 53

Let and let be a pointed model which is well-formed w.r.t. and such that . Then, there is a -segment of such that and for each , .

Proof

The proof is by induction on , for which there are two cases. Recall that .

(1) and : let be any -segment of . By hypothesis . Since every refinement of is also a refinement of , it follows that . Thus, it suffices to show that for each , . Fix and let be an infinite word over such that . Since is well-formed w.r.t. , as well. Let be a j-segment of such that . By definition of , . Thus, since , we deduce that . There are two cases: •

(base step): by construction,  is a singleton, , and  is a quantification-free -formula in positive normal form. Since  and , by Lemma 51, it follows that .

•

(induction step): since  and , by the induction hypothesis (note that since  is minimal, for each j-segment of , ), it follows that .

Thus, in both cases . Since is an arbitrary infinite word over such that , we obtain that , and the result follows.

(2), , and (induction step): since, there is a refinement of satisfying both and . By definition of , is well-formed w.r.t. j. Thus, since and , by the induction hypothesis, there is a j-segment of such that , , and for each , . Since is a refinement of , it easily follows that is the refinement of some -segment of . Since , it holds that . Hence, it suffices to show that for each , . Let . Then, since (resp., ) is minimal and well-formed w.r.t. (resp., j) and is a refinement of , it follows that there is such that . Since , we obtain that , and the result follows.  □

Now, we can prove the correctness of the construction.

Theorem 54

φ is satisfiable if, and only if, is satisfiable.

Proof

First, assume that is satisfiable. Hence, there is a pointed model which satisfies both and . By definition of formula , it follows that is well-formed w.r.t. 0. Since , by Lemma 53, we deduce that there is an infinite word w over such that . Since , it follows that φ is satisfiable.

Now, assume that φ is satisfiable. Since any proposition in P does not occur free in φ, it follows that for each infinite word w over , . Let be any pointed model which is well-formed w.r.t. 0. By definition of formula , it holds that . Moreover, since for each , and , by Lemma 52 it follows that . Therefore, . Hence, is satisfiable. □

By using Theorem 48 and the fact that there exists a linear time translation of into (see page 331) we now obtain the required proof of Theorem 44.

7.2. Succinctness

In this section we establish the following result.

Theorem 55

is doubly exponentially more succinct than , and  is doubly exponentially more succinct than modal μ-calculus.

Theorem 55 directly follows from the following result whose proof is given in the rest of this section.

Proposition 56

There is a finite set P of propositional variables and a family of one-agent formulas over P such that for each , has size and refining quantifier alternation depth 2, and each equivalent one-agent formula has size at least .11

Construction of the formulas in Proposition 56 Let . An n-configuration is a string on of length exactly . We define a class of pointed models, where each pointed model in the class encodes, in a suitable way, a pair of n-configurations. Then, we construct the formula in such a way that the following holds: a pointed model satisfies iff the two n-configurations encoded by coincide. In order to formally define the class , we need additional definitions. An n-block is a pair such that and . We say that c is the content of bl and i is the position of bl. Intuitively, bl represents the ith symbol of some n-configuration. First, we define an encoding of by a set of strings over of length . Since , i can be encoded by a binary string over of length exactly . Moreover, we keep track, for each , of the binary encoding (a string over of length n)12 of the position j of the jth bit in the binary encoding of i. This leads to the following definition. An n-sub-block is a string over of length of the form , where . The content of sbl is B and the position of sbl is the integer whose binary encoding is . Intuitively, sbl encodes the position and the content B of a bit along the binary encoding of an integer . Then, is the set of strings over of length such that • for each , , where sbl is an n-sub-block whose position j and content b satisfy the following: b is the jth bit in the binary encoding of i.

• for each , let be the jth bit in the binary encoding of i and be the n-sub-block whose position is j and whose content is . Then, .

Let be a pointed model over P. We denote by the set of finite or infinite strings over of the form such that is a maximal path of M starting from s. A pointed model encodes an n-block if ◇ ◇ Note that the set of pointed models encoding is nonempty. Let be a pair of n-configurations. A pointed model encodes the pair if it holds that: • s has two successors and (called the left successor and right successor of s, respectively). Moreover, , and ;

• for each , has successors . Moreover, for each , encodes the n-block , where is the ith symbol of the n-configuration .

If additionally, then we say that is balanced. The class is the class of pointed models such that encodes some pair of n-configurations. In order to define the formula (for each ), we first show Lemma 57. This lemma asserts that there is an formula of size which allows one to select, for a given pointed model , only the n-blocks encoded by having the same position.

Lemma 57

For each , one can construct a one-agent formula of size and refinement quantifier alternation depth 1 satisfying the following for all pairs of n-configurations: for each encoding the pair and each refinement of , •

satisfies  iff there is  such that the set of #-states (i.e. states whose label is )  reachable from  is nonempty and for each of such states , encodes an n-block whose position is i and whose content is either the ith symbol of  or the ith symbol of .

Proof

The formula is defined as follows: where and are formulas defined as follows: ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ ◇ Note that has size and that (refinement alternation depth). Thus, it remains to prove the second part of the lemma. Fix encoding some pair of n-configurations, and let be a refinement of . By construction, for each #-state reachable from in, there is a #-state reachable from s in M such that is a refinement of . Moreover, encodes some n-block , where the content c is either the ith symbol of or the ith symbol of . Thus, by definition of , we obtain the following.

Fact 1:  satisfies iff the set of #-states reachable from is nonempty and for each of such states , encodes some n-block , where the content c is either the ith symbol of or the ith symbol of .

In the second conjunct of the definition of, the formula intuitively enforces one to select the refinements of encoding only n-blocks having the same position. Formally, by definition of , we obtain the following.

Fact 2: Let be a refinement of . Then, satisfies iff for all , and the n-sub-block in u and the n-sub-block in have the same position.

Thus, by Fact 2 it follows that the second conjunct of definition of requires that all the n-sub-blocks in having the same position have also the same content, i.e., all the n-blocks encoded by have the same position. Thus, by Fact 1 the result follows.  □

For each , let be the formula satisfying the statement of Lemma 57. Then, the one-agent formula is defined as follows: By construction and Lemma 57, we easily obtain the following result.

Lemma 58

For each, the formula has size and (refinement alternation depth). Moreover, for each , satisfies iff is balanced.

Proof of Proposition 56

By Lemma 58, in order to complete the proof of Proposition 56, we need to show that for each , each one-agent formula equivalent to has size at least . For this, we use a well-known automata-characterization of (one-agent) in terms of parity symmetric alternating (finite-state) automata () which operate on pointed models [61]. First, we recall the class of . We need additional definitions.

A tree T is a prefix closed subset of ⁎ . The elements of T are called nodes and the empty word ε is the root of T. For, the set of children of x (in T) is . A path of T is a maximal sequence of T-nodes such that and for any i, is a child of . For an alphabet Σ, a Σ-labeled tree is a pair where T is a tree and . For a set X, denotes the set of positive boolean formulas over X, built from elements in X using ∨ and ∧ (we also allow the formulas true and false). A subset Y of X satisfies iff the truth assignment that assigns true to the elements in Y and false to the elements of satisfies θ.

A parity symmetric alternating automaton () over P is a tuple , where Q is a finite set of locations, is an initial location, ◇

is the transition function, and  is a parity acceptance condition assigning to each location an integer (called priority). Intuitively, a target of a move of  is encoded by an element in

◇ . An atom ◇

means that from the current state s (of the pointed input model) A moves to some successor of s and the location is updated to q. On the other hand, an atom  means that from the current state s the automaton splits in multiple copies and, for each successor  of s, one of such copies moves to  and the location is updated to q.

Formally, for a pointed model over P, a run of over is a -labeled tree .13 Moreover, we require that (initially, is in the initial location reading state ), and for each with, there is a (possibly empty) minimal set ◇

satisfying  such that the set  of labels of children of y in T is the smallest set satisfying the following: for all atoms ,

• if ◇ , then for some successor of s in M, ;

• if, then for each successor of s in M, .

For an infinite path of T, let be the set of locations in Q that appear in infinitely often. The run is accepting if for each infinite path π of T, the smallest priority of the locations in is even. The language of is the set of pointed models over P such that has an accepting run over . The following is a well-known result.

Proposition 59

(See [61].) Given a one-agent formula φ over P, one can construct a with locations whose language is the set of pointed models over P satisfying φ.

Proposition 56 directly follows from Proposition 59 and the following result.

Lemma 60

Let and be a over P whose language is the set of pointed models satisfying the formula . Then, the number of locations of is at least .

Proof

Let and as in the statement of the lemma (note that exists by Proposition 59 together with Proposition 42), and Q be the set of -locations. For each n-configuration w, let be some balanced pointed model encoding the pair , and be the set of sets such that there is an accepting run of over the pointed model so that: •

is the set of locations associated with the replicas of  in the run which read the left successor of in , i.e.,  for some . (Note that  if  does not visit the left successor  of .)

First, we show that . By hypothesis and Lemma 58, there must exist some accepting run of over the input . Now, by construction, is a set of subsets of Q, and is non-empty if and only if there is some accepting run of over . (If no accepting run of visits the left successor of in, then is a singleton containing just the empty set.) Hence, non-emptiness of follows. Next, we prove the following.

Claim

for all n-configurations w and such that , .

Proof of the claim

for a model M and a set, the restriction of M to is defined in the obvious way. For , let denote the restriction of M to the set of states reachable from s in M. For all n-configurations w and , let be the dir-successor of in . We prove the claim by contradiction. So, assume that there are two distinct n-configurations w and such that . Without loss of generality we can assume that and have no states in common. Let be any pointed model satisfying the following: the successors of in are and , and and . Evidently, is a pointed model encoding the pair . Since , by hypothesis and Lemma 58, does not accept . On the other hand, since there is , by definition of the sets and and the semantics of , it easily follows that there is an accepting run of over , which is a contradiction. Hence, the claim holds.

By the claim above, it follows that for each n-configuration w, there is (recall that ) such that for all n-configurations distinct from w, . Since the number of distinct n-configurations is and the number of subsets of Q is , we obtain that , and the result holds.  □

8. Conclusions and perspectives

Conclusions

We conclude that we hope to have established a platform for structural refinement in various modal logics. We established results on axiomatization, complexity, expressivity, and we gave applications to software verification and design, and to dynamic epistemic logics. We clearly established the relation to bisimulation quantified logics: refinement quantification is bisimulation followed by relativization. The multi-agent refinement modal logic and the furthest generalization in the form of refinement μ-calculus are only the beginning. One could think of refinement CTL, refinement PDL, (yet other) refinement epistemic logics, refinement with further structural restrictions or with protocol restrictions, and so on. Each of these logics may have different axiomatizations and complexities, and equal expressivity as the logic without refinement is certainly not to be expected; e.g., we estimate that refinement modal logic is more expressive than the base modal logic on the model class.

Recent results

Following the initial submission of the paper, some further results have been obtained in this area, typically involving one of the authors. In [12] it was established that the complexity of refinement modal logic for a single agent is -complete, which means that the satisfiability of an formula can be decided by an exponential-time bounded Alternating Turing Machine with a linearly-bounded number of alternations. In [28] an axiomatization of the multi-agent refinement modal logic of knowledge is given, among other results. As a generalization of quantifying over announcements (arbitrary announcements), in [8] semantics were also given for quantifying over action models and the question was posed how to axiomatize this logic: in [26] it is shown that quantifying over action models is equally expressive as the refinement quantifier, i.e., ‘there is a refinement after which φ is true’ means the same as ‘there is an action model such that after its execution φ is true’. This answers one of the open questions on logics with quantification over information change, posed in the recent survey [54]. That survey also puts various other proposals on propositional quantification in perspective, such as [52], [18], [7] (going back to [6]), and [60] — for details, see [54]. It should not be forgotten to mention that many of these, including our own proposal, go back to the original publication [21].

Further research

We wish to determine the complexity of model checking in the various refinement modal logics. On the further horizon loom the detailed investigation of other refinement logics, mainly refinement PDL and refinement CTL, and the exploration of their applications. The relation of refinement quantification to other forms of propositional quantification over information change also needs further investigation.

Acknowledgments

We acknowledge a very insightful and detailed review from a journal referee. Hans van Ditmarsch is also affiliated to IMSc (Institute of Mathematical Sciences), Chennai, India. We acknowledge support from ERC project EPS 313360, and from EU 7th Framework Programme under grant agreement no. 295261 (MEALS).

References

;

	Author	volume	Date Value	title	type	journal	titleUrl	doi	note	year
2014 RefinementModalLogic	Laura Bozzelli Hans van Ditmarsch Tim French James Hales Sophie Pinchinat			Refinement Modal Logic				10.1016/j.ic.2014.07.013		2014