Positive Hennessy-Milner Logic for Branching Bisimulation

2025-05-02 0 0 524.54KB 22 页 10玖币

侵权投诉

POSITIVE HENNESSY-MILNER LOGIC FOR BRANCHING

BISIMULATION

HERMAN GEUVERS aAND KOMI GOLOV a

Radboud University Nijmegen, The Netherlands

e-mail address: herman@cs.ru.nl, a.golov@math.ru.nl

Abstract.

Labelled transitions systems can be studied in terms of modal logic and in

terms of bisimulation. These two notions are connected by Hennessy-Milner theorems,

that show that two states are bisimilar precisely when they satisfy the same modal logic

formulas. Recently, apartness has been studied as a dual to bisimulation, which also gives

rise to a dual version of the Hennessy-Milner theorem: two states are apart precisely when

there is a modal formula that distinguishes them.

In this paper, we introduce “directed” versions of Hennessy-Milner theorems that

characterize when the theory of one state is included in the other. For this we introduce

“positive modal logics” that only allow a limited use of negation. Furthermore, we introduce

directed notions of bisimulation and apartness, and then show that, for this positive modal

logic, the theory of

is included in the theory of

precisely when

is directed bisimilar to

Or, in terms of apartness, we show that

is directed apart from

precisely when the theory

is not included in the theory of

. From the directed version of the Hennessy-Milner

theorem, the original result follows.

In particular, we study the case of branching bisimulation and Hennessy-Milner Logic

with Until (HMLU) as a modal logic. We introduce “directed branching bisimulation” (and

directed branching apartness) and “Positive Hennessy-Milner Logic with Until” (PHMLU)

and we show the directed version of the Hennessy-Milner theorems. In the process, we

show that every HMLU formula is equivalent to a Boolean combination of Positive HMLU

formulas, which is a very non-trivial result. This gives rise to a sublogic of HMLU that is

equally expressive but easier to reason about.

Concurrent systems are usually modeled as labelled transition systems (LTS), where a

labelled transition step takes one from one state to the other in a non-deterministic way.

Two states in such a system are considered equivalent in case the same labelled transitions

can be taken to equivalent states. This is captured via the notion of bisimulation, which is a

type of observable equality: two states are bisimilar if we can make the same observations

on them, where the observations are the labelled transitions to equivalent states.

Often it is the case that some transitions cannot be observed and then they are modeled

via a silent step, also called a

-step, denoted by

t→τs

. The notion of bisimulation should

take this into account and abstract away from the silent steps. This leads to a notion of weak

bisimulation (as opposed to strong bisimulation, where all steps are observable). In [

vGW89

]

(and the later full version [

vGW96

]) it has been noticed that weak bisimulation ignores the

branching in an LTS that can be caused by silent steps, and that is undesirable. Therefore

Key words and phrases: bisimulation apartness concurrency.

Preprint submitted to

Logical Methods in Computer Science

⃝Creative Commons

arXiv:2210.07380v3 [cs.LO] 22 Oct 2024

2 H. GEUVERS AND K. GOLOV

the notion of branching bisimulation has been developed, which ignores the silent steps while

taking into account their branching behavior. Branching bisimulation has been studied a lot

as it is the ﬁnest equivalence in the well-known “van Glabbeek spectrum” [

vG93

]. Various

algorithms have been developed for checking branching bisimulation and various tools have

been developed that verify branching bisimulation for large systems [GV90, JGKW20].

There is a well-known connection between notions of bisimulation and various modal

logics, ﬁrst discovered by Hennessy and Milner [

HM85

] for strong bisimulation, and then

extended to weak and branching bisimulation by De Nicola and Vaandrager [

dNV95

]. Let

↔

be a bisimilarity relation, and let

(

) be the set of formulas in some modal logic that

are true in

. A Hennessy-Milner theorem is a theorem relating the bisimulation and the

logic by showing that two states are bisimilar precisely when their theories coincide:

s↔t⇐⇒ Th(s) = Th(t).

Hennessy and Milner proved such a theorem for Hennessy-Milner Logic and strong

bisimulation, while De Nicola and Vaandrager extended this to Hennessy-Milner Logic

and

weak bisimulation, and Hennessy-Milner Logic with Until and branching bisimulation.

In this paper, we explore what a directed variant of such a theorem would look like by

considering what form of “directed bisimulation” relation corresponds to inclusion of theories.

Hennessy-Milner logics typically have negation, so if the theory of one state is included in

the other, then they are equal. As a consequence, Hennessy-Milner logics typically do not

permit non-trivial inclusions of theories, so we must ﬁrst replace the logic with a positive

version. Writing

→

for our new relation and

ThP

(

) for the theory of

in this new, positive,

logic, we prove the property

s→t⇐⇒ ThP(s)⊆ThP(t).(0.1)

Our constructions ensure that

s↔t

precisely when

s→t

and

t→s

, and that

ThP

(

) =

ThP

(

) precisely when

(

) =

(

). The undirected Hennessy-Milner theorem

is thus an immediate consequence of our directed variant.

Our proof of Equation (0.1) uses the notion of apartness, which is the dual notion of

bisimulation, studied previously by Geuvers and Jacobs [

GJ21

]. Two states are bisimilar

precisely when they are not apart. The property we prove is thus

s#> t ⇐⇒ ∃φ. φ ∈ThP(s)−ThP(t),(0.2)

where φis called the distinguishing formula.

Unlike bisimulation, apartness is an inductive notion, meaning that we can perform our

proofs by an induction on the derivation of an apartness. It turns out that the structure of

this derivation closely mirrors the distinguishing formula, making the proof straightforward.

This was previously shown by Geuvers in relation to strong and weak bisimulation in [

Geu22

but a straightforward inductive proof does not work in the branching setting when the logic

includes an until operator.

In this paper we study the directed constructions for branching bisimulation. Concretely,

we deﬁne and study (Section 2) a logic PHMLU of Positive Hennessy-Milner Logic with

Until formulas (Subsection 2.1), as well as a directed branching bisimulation relation

→db

(Subsection 2.2) and a directed branching apartness relation

#>db

(Subsection 2.3). We

then show that Equation (0.2) (for PHMLU and branching apartness) holds, and from that

we conclude that Equation (0.1) holds as well. There are diﬀerences between HMLU and

1This involved modifying the semantics to account for silent steps.

POSITIVE HENNESSY-MILNER LOGIC FOR BRANCHING BISIMULATION 3

PHMLU that make it far from obvious that the logics are equally powerful. We show that

the logics are equivalent in which states they distinguish, and moreover we show that every

HMLU formula is equivalent to a Boolean combination of PHMLU formulas (Subsection 2.1).

This gives rise to a logic that is equally expressive as HMLU, but for which the satisfaction

relation is simpler.

To introduce the directed versions of bisimulation and apartness, and the corresponding

positive modal logics, we will ﬁrst start from the simpler setting of strong bisimulation

and standard Hennessy-Milner Logic in Section 1. Here the construction and the proofs

are rather straightforward, but it also suggests that a ‘directed approach’ to bisimulation,

combined with a positive version of Hennessy-Milner logic and the use of apartness, should

be applicable to other notions of bisimulation. For weak bisimulation, this is the case, which

we have veriﬁed, but not included in the present paper.

Throughout this paper, we will work in a ﬁxed labelled transition system (LTS) (

X, A, →

consisting of a set of states

, a set of actions

, possibly with a silent action

τ̸∈ A

, and a

transition relation

→a

for every

a∈A

(and for

, if applicable). Following [

GJ21

], we will

use

to denote an arbitrary action from

A∪ {τ}

to denote an arbitrary non-silent action

(so

a∈A

), and use

↠α

to denote the transitive reﬂexive closure of

→α

. We use

→(α)

as a

shorthand for →aif α=a̸=τ, and for the reﬂexive closure of →τif α=τ.

We would like to thank Jan Friso Groote and Jurriaan Rot for discussions on the topic

of this paper.

1. Hennessy-Milner Logic and Strong Bisimulation

Deﬁnition 1.1. Alabelled transition system (LTS) is a tuple (

X, A, →

), where

is a set

of states,

is a set of actions and for every

a∈A

→a

is a binary relation on

. When

s→atholds, we say that s a-steps to t.

An LTS is image-ﬁnite if for all s∈Xand a∈A, the set {t∈X|s→aq}is ﬁnite.

We will be particularly interested in image-ﬁnite LTSs, since the logics we study are

ﬁnitary. We can characterize states in an LTS using Hennessy-Milner Logic (HML).

Deﬁnition 1.2. The formulas of HML are given inductively by the following deﬁnition:

φ:= ⊤ | ¬φ|φ1∧φ2| ⟨a⟩φ.

We say that a formula of the form

⟨a⟩φ

is a modal formula. We use

⊥

as a shorthand

for

¬⊤

and

φ1∨φ2

as a shorthand for

(

¬φ1∧ ¬φ2

). The modality binds weakly;

⟨a⟩φ∧ψ

denotes ⟨a⟩(φ∧ψ).

Deﬁnition 1.3. The relation s⊨φis deﬁned inductively by the following rules:

s⊨⊤always s⊨φ1∧φ2⇔s⊨φ1and s⊨φ2

s⊨¬φ⇔s̸⊨φ s ⊨⟨a⟩φ⇔ ∃s′. s →as′∧s′⊨φ.

Given a state

we deﬁne

(

) :=

{φ∈HML |s⊨φ}

, the set of HML formulas true in

. We call a formula in

(

)

−Th

(

) or

(

)

−Th

(

) a distinguishing formula for

and

To compare two states, one considers if they can recursively simulate one another. This

notion is known as bisimulation.

4 H. GEUVERS AND K. GOLOV

Deﬁnition 1.4. A symmetric relation

is a strong bisimulation if whenever

(

s, t

) and

s→as′, there exists some t′such that R(s′, t′) and t→at′.

We say two states are strongly bisimilar (notation

s↔st

) if there exists a strong

bisimulation that relates them.

A key result of Hennessy and Milner [

HM85

] is that these two views of labelled transition

systems are related in the following sense:

Theorem 1.5 [

HM85

].In an image-ﬁnite LTS, two states

and

are strongly bisimilar

precisely when they satisfy the same HML formulas; that is,

s↔st⇔Th(s) = Th(t).

We are interested in a similar theorem that considers inclusion of theories rather than

equality. However, in the context of Hennessy-Milner Logic such a theorem would not be

meaningfully diﬀerent, since the presence of negation gives us the following result:

Proposition 1.6. If Th(s)⊆Th(t), then Th(s) = Th(t).

Proof.

Suppose, on the contrary, that there is some

φ∈Th

(

)

−Th

(

). Then

¬φ∈Th

(

)

⊆

Th(t), hence t⊨φand t⊨¬φ, a contradiction.

We will thus introduce Positive Hennessy-Milner Logic (PHML), where negation is only

permitted under a modality.2

Deﬁnition 1.7. The formulas of PHML are given inductively by the following deﬁnition:

φ:= ⊤ | ⊥ | φ1∧φ2|φ1∨φ2| ⟨a⟩(φ1∧ ¬φ2).

We view a formula of PHML as also being a formula of HML, and can thus reuse

the semantics from Deﬁnition 1.3. We deﬁne

ThP

(

) :=

{φ∈PHML |s⊨φ}

. We call a

φ∈ThP(s)−ThP(t) a positive distinguishing formula for sand t.

There are various syntactic classes related to PHML that will be useful for our proofs,

and for these we introdice some special notation.

Notation 1.8.

• ±PHML denotes the set of PHML formulas and their negations.

•V±PHML denotes the set of conjunctions of ±PHML formulas.

•

Given a formula

φ∈V±PHML

, we will use

φ+

and

φ−

to refer to the PHML formulas

such that φis equivalent to φ+∧ ¬φ−.

φ+

is the conjunction of all ‘positive’ conjuncts of

, the positive segment of

, and

φ−

is the disjunction of

for every ‘negative’ conjunct

¬ψ

, the negative segment of

Concretely, for

φ∈V±PHML

with

φ1∧φ2∧ ¬φ3∧ ¬φ4

, we have

φ+

φ1∧φ2

and

φ−

φ3∨φ4

, and so

is equivalent to

φ+∧ ¬φ−

. We write

⟨a⟩φ

for

⟨a⟩φ+∧ ¬φ−

. Recall

that by our conventions, this is read as ⟨a⟩(φ+∧ ¬φ−).

Example 1.9. If we consider PHML, we can have non-trivial inclusion of theories. This is

illustrated by the following LTS.

Prohibiting negation entirely would produce a logic that is too weak; it would correspond to simulation.

Two states simulating each other is weaker than two states being bisimilar, while we require that two states

directed bisimulating each other be equivalent to the states being bisimilar.

POSITIVE HENNESSY-MILNER LOGIC FOR BRANCHING BISIMULATION 5

In this LTS, we have

ThP

(

)

⊊ThP

(

)

⊊ThP

(

). Examples of PHML formulas that

distinguish s,tand rare the following.

• ⟨a⟩⟨a⟩⊤, which holds in sbut not in tand r.

• ⟨a⟩¬⟨a⟩⊤ and ⟨a⟩⊤, which hold in sand t, but not in r

Note that

⟨a⟩⊥

does not hold in any state, but for diﬀerent reasons: in

there is no

-step

possible, whereas in

and

there is an

-step possible, but not to a state where

⊥

holds

(because ⊥never holds).

Theorem 1.10. Every HML formula

is equivalent to a disjunction of

V±PHML

formulas.

Proof.

The proof proceeds by induction on

. We treat the cases for

being a negation

and for φbeing a modality.

Suppose that

¬ψ

, then by induction there is a formula

i=1

equivalent to

and we write Ψ

= Ψ

i∧ ¬

−

(for

i∈ {

, . . . , n}

). Then

¬ψ

is equivalent to

i=1 ¬

(Ψ

)

∨

−

. Note that Ψ

−

i∈PHML

, but

(Ψ

) is a negation of a

PHML

-formula.

We can let

∧

distribute over

∨

and we ﬁnd that

is equivalent to a disjunction of

V±PHML

formulas.

Suppose that

⟨a⟩ψ

, then by induction there is a formula

Wi∈I

equivalent to

Since modality distributes over disjunction,

⟨a⟩Wi

is equivalent to

Wi⟨a⟩

, which is the

desired formula.

Corollary 1.11. For all states

s, t

, we have

(

) =

(

)precisely when

ThP

(

) =

ThP

(

Proof.

The left to right direction is easy:

ThP

(

) =

(

)

∩PHML

, so

(

) =

(

) implies

ThP(s) = ThP(t).

In the other direction, suppose

ThP

(

) =

ThP

(

) and

φ∈Th

(

). By Theorem 1.10,

there is an equivalent formula

where Ψ

i∈V±PHML

. As

s⊨φ

, there is some

such

that

s⊨

. Writing Ψ

j∧ ¬

−

, we have that for all

s⊨

and

s̸⊨

−

. Since

each Ψ

and Ψ

−

is positive, it follows that

t⊨

and

t̸⊨

−

and thus

t⊨

and

t⊨φ

, as

required.

This concludes our construction on the logic side. Let us now consider the bisimulation

side of the question.

Deﬁnition 1.12. A relation

is a directed strong bisimulation if whenever

(

s, t

) and

s→as′, there exists some t′such that t→at′and R(s′, t′) and R(t′, s′).

We say two states are directed strongly bisimilar (notation

s→ds t

) if there exists a

directed strong bisimulation that relates them.

Theorem 1.13. Two states are strongly bisimilar if and only if they are directed strongly

bisimilar in each direction.

Proof.

The left-to-right direction follows from the fact that every strong bisimulation is a

directed strong bisimulation. The other direction follows from

↔ds

itself being a strong

bisimulation.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

POSITIVEHENNESSY-MILNERLOGICFORBRANCHINGBISIMULATIONHERMANGEUVERSaANDKOMIGOLOVaRadboudUniversityNijmegen,TheNetherlandse-mailaddress:herman@cs.ru.nl,a.golov@math.ru.nlAbstract.Labelledtransitionssystemscanbestudiedintermsofmodallogicandintermsofbisimulation.ThesetwonotionsareconnectedbyHennessy-Miln...

展开>> 收起<<

Positive Hennessy-Milner Logic for Branching Bisimulation.pdf

共22页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Positive Hennessy-Milner Logic for Branching Bisimulation

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: