Synthesizing Dominant Strategies for Liveness Full Version

2025-05-02 0 0 805.55KB 33 页 10玖币

侵权投诉

Synthesizing Dominant Strategies for Liveness

(Full Version)

Bernd Finkbeiner !

CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Noemi Passing !

CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Abstract

Reactive synthesis automatically derives a strategy that satisﬁes a given speciﬁcation. However,

requiring a strategy to meet the speciﬁcation in every situation is, in many cases, too hard of a

requirement. Particularly in compositional synthesis of distributed systems, individual winning

strategies for the processes often do not exist. Remorsefree dominance, a weaker notion than winning,

accounts for such situations: dominant strategies are only required to be as good as any alternative

strategy, i.e., they are allowed to violate the speciﬁcation if no other strategy would have satisﬁed it

in the same situation. The composition of dominant strategies is only guaranteed to be dominant

for safety properties, though; preventing the use of dominance in compositional synthesis for liveness

speciﬁcations. Yet, safety properties are often not expressive enough. In this paper, we thus introduce

a new winning condition for strategies, called delay-dominance, that overcomes this weakness of

remorsefree dominance: we show that it is compositional for many safety and liveness speciﬁcations,

enabling a compositional synthesis algorithm based on delay-dominance for general speciﬁcations.

Furthermore, we introduce an automaton construction for recognizing delay-dominant strategies and

prove its soundness and completeness. The resulting automaton is of single-exponential size in the

squared length of the speciﬁcation and can immediately be used for safraless synthesis procedures.

Thus, synthesis of delay-dominant strategies is, as synthesis of winning strategies, in 2EXPTIME.

2012 ACM Subject Classiﬁcation Theory of computation

Keywords and phrases Dominant Strategies, Compositional Synthesis, Reactive Synthesis

Related Version A conference version of this paper is available at [19].

Funding

This work was supported by DFG grant 389792660 as part of TRR 248 (CPEC) and

by ERC grant 683300 (OSARES). N. Passing is a PhD candidate at Saarland University, Germany.

1 Introduction

Reactive synthesis is the task of automatically deriving a strategy that satisﬁes a formal

speciﬁcation, e.g., given in LTL [

], in every situation. Such strategies are called winning.

In many cases, however, requiring the strategy to satisfy the speciﬁcation in every situation is

too hard of a requirement. A prominent example is the compositional synthesis of distributed

systems consisting of several processes. Compositional approaches for distributed synthesis [

] break down the synthesis task for the whole system into several smaller ones for

the individual processes. This is necessary due to the general undecidability [

] of distributed

synthesis and the non-elementary complexity [

] for decidable cases: non-compositional

distributed synthesis approaches [

] suﬀer from a severe state space explosion problem

and are thus not feasible for larger systems. However, winning strategies rarely exist when

considering the processes individually in the smaller subtasks of compositional synthesis since

usually the processes need to collaborate in order to achieve the overall system’s correctness.

For instance, a particular input sequence may prevent the satisfaction of the speciﬁcation

no matter how a single process reacts, yet, the other processes of the system ensure in the

interplay of the whole system that this input sequence will never be produced.

arXiv:2210.01660v2 [cs.LO] 14 Feb 2023

2 Synthesizing Dominant Strategies for Liveness (Full Version)

Remorsefree dominance [

], a weaker notion than winning, accounts for such situations.

A dominant strategy is allowed to violate the speciﬁcation as long as no other strategy would

have satisﬁed it in the same situation. Hence, a dominant strategy is a best-eﬀort strategy

as we do not blame it for violating the speciﬁcation if the violation is not its fault. Searching

for dominant strategies rather than winning ones allows us to ﬁnd strategies that do not

necessarily satisfy the speciﬁcation in all situations but in all that are realistic in the sense

that they occur in the interplay of the processes if all of them play best-eﬀort strategies.

The parallel composition of dominant strategies, however, is only guaranteed to be domi-

nant for safety properties [

]. For liveness speciﬁcations, in contrast, dominance is not a

compositional notion and thus not suitable for compositional synthesis. Consider, for example,

a system with two processes

and

sending messages to each other, denoted by atomic

propositions

and

, respectively. Both processes are required to send their message

eventually, i.e.,

m1∧m2

. For

, it is dominant to wait for the other process to send

the message

m3−i

before sending its own message

: if

p3−i

sends its message eventually,

does so as well, satisfying

. If

p3−i

never sends its message,

is violated, no matter how

reacts, and thus the violation of

is not

’s fault. Combining these strategies for

and

however, yields a system that never sends any message since both processes wait indeﬁnitely

for each other, while there clearly exist strategies for the whole system that satisfy ϕ.

Bounded dominance [

] is a variant of remorsefree dominance that ensures composition-

ality of general properties. Intuitively, it reduces every speciﬁcation

to a safety property

by introducing a measure of the strategy’s progress with respect to

, and by bounding

the number of non-progress steps, i.e., steps in which no progress is made. Yet, bounded

dominance has two major disadvantages: (i) it requires a concrete bound on the number of

non-progress steps, and (ii) not every bounded dominant strategy is dominant: if the bound

is chosen too small, every strategy, also a non-dominant one, is trivially n-dominant.

In this paper, we introduce a new winning condition for strategies, called delay-dominance,

that builds upon the ideas of bounded dominance but circumvents the aforementioned

weaknesses. Similar to bounded dominance, it introduces a progress measure on strategies.

However, it does not require a concrete bound on the number of non-progress steps but

relates such steps in the potentially delay-dominant strategy

to non-progress steps in an

alternative strategy

: intuitively,

delay-dominates

if, whenever

makes a non-progress

step,

makes a non-progress step eventually as well. A strategy

is then delay-dominant if it

delay-dominates every other strategy

. In this way, we ensure that a delay-dominant strategy

satisﬁes the speciﬁcation “faster” than all other strategies in all situations in which the

speciﬁcation can be satisﬁed. Delay-dominance considers speciﬁcations given as alternating

co-Büchi automata. Non-progress steps with respect to the automaton are those that enforce

a visit of a rejecting state in all run trees. We introduce a two-player game, the so-called

delay-dominance game, which is vaguely leaned on the delayed simulation game for alternating

Büchi automata [

], to formally deﬁne delay-dominance: the winner of the game determines

whether or not a strategy sdelay-dominates a strategy ton a given input sequence.

We (i) show that every delay-dominant strategy is also remorsefree dominant, and (ii) in-

troduce a criterion for automata such that, if the criterion is satisﬁed, compositionality of

delay-dominance is guaranteed. The criterion is satisﬁed for many automata; both ones

describing safety properties and ones describing liveness properties. Thus, delay-dominance

overcomes the weaknesses of both remorsefree and bounded dominance. Note that since

delay-dominance relies, as bounded dominance, on the automaton structure, there are realiz-

able speciﬁcations for which no delay-dominant strategy exists. Yet, we experienced that

this rarely occurs in practice when constructing the automaton from an LTL formula with

standard algorithms. Moreover, if a delay-dominant strategy exists, it is guaranteed to be

winning if the speciﬁcation is realizable. Hence, the parallel composition of delay-dominant

B. Finkbeiner and N. Passing 3

strategies for all processes in a distributed system is winning for the whole system as long

as the speciﬁcation is realizable and as long as the compositionality criterion is satisﬁed.

Therefore, delay-dominance is a suitable notion for compositional synthesis.

We thus introduce a synthesis approach for delay-dominant strategies that immediately

enables a compositional synthesis algorithm for distributed systems, namely synthesizing

delay-dominant strategies for the processes separately. We present the construction of a

universal co-Büchi automaton

Add

Aϕ

from an LTL formula

that recognizes delay-dominant

strategies.

Add

Aϕ

can immediately be used for safraless synthesis [

] approaches such as

bounded synthesis [

] to synthesize delay-dominant strategies. We show that the size of

Add

Aϕ

is single-exponential in the squared length of

. Thus, synthesis of delay-dominant strategies

is, similar to synthesis of winning or remorsefree dominant strategies, in 2EXPTIME.

Related Work.

Remorsefree dominance has ﬁrst been introduced for reactive synthesis in [

Dominant strategies have been utilized for compositional synthesis of safety properties [10].

Building up on this work, a compositional synthesis algorithm, that ﬁnds solutions in more

cases by incrementally synthesizing individual dominant strategies, has been developed [

Both algorithms suﬀer from the non-compositionality of dominant strategies for liveness

properties. Bounded dominance [

], a variant of dominance that introduces a bound on the

number of steps in which a strategy does not make progress with respect to the speciﬁcation,

solves this problem. However, it requires a concrete bound on the number of non-progress

steps. Moreover, a bounded dominant strategy is not necessarily dominant.

Good-enough synthesis [

] follows a similar idea as dominance. It is thus not composi-

tional for liveness properties either. In good-enough synthesis, conjuncts of the speciﬁcation

can be marked as strong. If the speciﬁcation is unrealizable, a good-enough strategy needs

to satisfy the strong conjuncts while it may violate the other ones. Thus, dominance can

be seen as the special case of good-enough synthesis in which no conjuncts are marked as

strong. Good-enough synthesis can be extended to a multi-valued correctness notion [1].

Synthesis under environment assumptions is a well-studied problem that also aims at

relaxing the requirements on a strategy. There, explicit assumptions on the environment are

added to the speciﬁcation. These assumptions can be LTL formulas restricting the possible

input sequences (see, e.g., [

]) or environment strategies (see, e.g., [

]). The

assumptions can also be conceptual such as assuming that the environment is rational (see,

e.g., [

]). Synthesis under environment assumptions is orthogonal to the synthesis

of dominant strategies and good-enough synthesis since it requires an explicit assumption on

the environment, while the latter two approaches rely on implicit assumptions.

2 Preliminaries

Notation.

Given an inﬁnite word

σ0σ1. . . ∈

)

, we denote the preﬁx of length

+ 1

with

σ|t

σ0. . . σt

. For

and a set

X⊆

Σ, let

σ∩X

:= (

σ0∩X

)(

σ1∩X

)

. . . ∈

)

For

σ∈

)

σ0∈

Σ0

)

with Σ

∩

∅

, we deﬁne

σ∪σ0

:= (

σ0∪σ0

)(

σ1∪σ0

)

. . . ∈

Σ∪Σ0

)

For a

-tuple

, we denote the

-th component of

with

(

). We represent a Boolean formula

WiVjci,j in disjunctive normal form (DNF) also in its set notation Si{Sj{ci,j }}.

LTL.

Linear-time temporal logic (LTL) [

] is a standard speciﬁcation language for linear-

time properties. Let Σbe a ﬁnite set of atomic propositions and let

a∈

Σ. The syntax

of LTL is given by

ϕ, ψ

::=

a| ¬ϕ|ϕ∨ψ|ϕ∧ψ|ϕ|ϕUψ

. We deﬁne

true

a∨ ¬a

false

¬true

true Uϕ

, and

¬ ¬ϕ

as usual. We use the standard semantics.

The language L(ϕ)of an LTL formula ϕis the set of inﬁnite words that satisfy ϕ.

4 Synthesizing Dominant Strategies for Liveness (Full Version)

Non-Alternating ω-Automata.

Given a ﬁnite alphabet Σ, a Büchi (resp. co-Büchi) au-

tomaton

= (

Q, Q0, δ, F

)over Σconsists of a ﬁnite set of states

, an initial state

q0∈Q

a transition relation

Q×

Σ×Q

, and a set of accepting (resp. rejecting) states

F⊆Q

For an inﬁnite word

σ0σ1. . . ∈

)

, a run of

induced by

is an inﬁnite sequence

q0q1. . . ∈Qω

of states with (

qi, σi, qi+1

)

∈δ

for all

i≥

0. A run is accepting if it contains

inﬁnitely many accepting states (resp. only ﬁnitely many rejecting states). A nondeterministic

(resp. universal) automaton

accepts a word

if some run is accepting (resp. all runs

are accepting). The language

(

)of

is the set of all accepted words. We consider

nondeterministic Büchi automata (NBAs) and universal co-Büchi automata (UCAs).

Alternating ω-Automata.

An alternating Büchi (resp. co-Büchi) automaton (ABA resp.

ACA)

= (

Q, q0, δ, F

)over a ﬁnite alphabet Σconsists of a ﬁnite set of states

, an initial

state q0⊆Q, a transition function δ:Q×2Σ→B+(Q), where B+(Q)is the set of positive

Boolean formulas over

, and a set of accepting (resp. rejecting) states

F⊆Q

. We assume

that the elements of

B+

(

)are given in DNF. Runs of

are

-labeled trees: a tree

is a

preﬁx-closed subset of N∗

. The children of a node x∈ T are c(x) = {x·d∈ T | d∈N}. An

-labeled tree (

T, `

)consists of a tree

and a labeling function

T → X

. A branch of

(

T, `

)is a maximal sequence

(

)

(

)

. . .

with

and

xi+1 ∈c

(

)for

i≥

0. A run

tree of

induced by

σ∈

)

is a

-labeled tree (

T, `

)with

(

) =

and, for all

x∈ T

(

)

|x0∈c

(

)

} ∈ δ

(

)

, σ|x|

). A run tree is accepting if every inﬁnite branch contains

inﬁnitely many accepting states (resp. only ﬁnitely many rejecting states).

accepts

there is some accepting run tree. The language L(A)of Ais the set of all accepted words.

Two-Player Games.

An arena is a tuple

= (

V, V0, V1, v0, E

), where

are ﬁnite

sets of positions with

V0∪V1

and

V0∩V1

∅

v0∈V

is the initial position,

E⊆V×V

is a set of edges such that

∀v∈V. ∃v0∈V.

(

v, v0

)

∈E

. Player

controls positions in

. A

game

= (

A, W

)consists of an arena

and a winning condition

W⊆Vω

. A play is an

inﬁnite sequence

ρ∈Vω

such that (

ρi, ρi+1

)

∈E

for all

i∈N

. The player owning a position

chooses the edge on which the play is continued. A play

is initial if

ρ0

holds. It is

winning for Player 0 if

ρ∈W

and winning for Player 1 otherwise. A strategy for Player

is a

function

V∗Vi→V

such that (

v, v0

)

∈E

whenever

(

w, v

) =

for some

w∈V∗

v∈Vi

A play

is consistent with a strategy

if, for all

j∈N

ρj∈Vi

implies

ρj+1

(

ρ|j

). A

strategy for Player iis winning if all initial and consistent plays are winning for Player i.

System Architectures.

An architecture is a tuple

= (

,inp,out

), where

is a set of

processes consisting of the environment

env

and a set

P−

P\{env}

system processes, Σ

is a set of Boolean variables,

inp

hI1, . . . , Ini

assigns a set

Ij⊆

Σof input variables to

each

pj∈P−

, and

out

hOenv, O1,...Oni

assigns a set

Oj⊆

Σof output variables to each

pj∈P

. For all

pj, pk∈P−

with

Ij∩Oj

∅

and

Oj∩Ok

∅

hold. The variables

Σj

pj∈P−

are given by

Σj

Ij∪Oj

. The inputs

, outputs

, and variables Σof the whole

system are deﬁned by

Spj∈P−Xj

for

X∈ {I, O,

}

is called distributed if

|P−

| ≥

In the remainder of this paper, we assume that a distributed architecture is given.

Process Strategies.

A strategy for process

is a function

: (2

)

∗→

mapping a

history of inputs to outputs. We model sias a Moore machine Mi= (T, t0, τ, o)consisting

of a ﬁnite set of states

, an initial state

t0∈T

, a transition function

T×

Ii→T

and a labeling function

T→

. For a sequence

γ0γ1. . . ∈

)

produces a

path (

t0, γ0∪o

(

))(

t1, γ1∪o

(

))

. . . ∈

(

T×

Ii∪Oi

)

, where

(

tj, γj

) =

tj+1

. The projection

B. Finkbeiner and N. Passing 5

of a path to the variables is called a trace. The trace produced by

γ∈

)

called the computation of

, denoted

comp

(

si, γ

). We say that

is winning for an

LTL formula

, denoted

si|

, if

comp

(

si, γ

)

holds for all input sequences

γ∈

)

Overloading notation with two-player games, we call a process strategy simply a strategy

whenever the context is clear. The parallel composition

Mi|| Mj

of two Moore machines

= (

Ti, ti

0, τi, oi

= (

Tj, tj

0, τj, oj

)for

pi, pj∈P−

is the Moore machine (

T, t0, τ, o

)

with inputs (

Ii∪Ij

)

(

Oi∪Oj

)and outputs

Oi∪Oj

as well as

Ti×Tj

= (

0, tj

τ((t, t0), ι)=(τi(t, (ι∪oj(t0)) ∩Ii), τj(t0,(ι∪oi(t)) ∩Ij)), and o((t, t0)) = oi(t)∪oj(t0).

Synthesis.

Given a speciﬁcation

, synthesis derives strategies

s1, . . . , sn

for the system

processes such that

s1|| · · · || sn|

, i.e., such that the parallel composition of the strategies

satisﬁes

for all input sequences generated by the environment. If such strategies exist,

called realizable. Bounded synthesis [

] additionally bounds the size of the strategies. The

search for strategies is encoded into a constraint system that is satisﬁable if, and only if,

realizable for the size bound. There are SMT, SAT, QBF, and DQBF encodings [

We consider a compositional synthesis approach that synthesizes strategies for the processes

separately. Thus, outputs produced by the other system processes are treated similar to

the environment outputs, namely as part of the input sequence of the considered process.

Nevertheless, compositional synthesis derives strategies such that

s1|| · · · || sn|

holds.

3 Dominant Strategies and Liveness Properties

Given a speciﬁcation

, the naïve compositional synthesis approach is to synthesize strategies

s1, . . . , sn

for the system processes such that

si|

holds for all

pi∈P−

. Then, it follows

immediately that

s1|| · · · || sn|

holds as well. However, since winning strategies are

required to satisfy

for every input sequence, usually no such individual winning strategies

exist due to complex interconnections in the system. Therefore, the naïve approach fails in

many cases. The notion of remorsefree dominance [

], in contrast, has been successfully used

in compositional synthesis [

]. The main idea is to synthesize dominant strategies for

the system processes separately instead of winning ones. Dominant strategies are, in contrast

to winning strategies, allowed to violate the speciﬁcation for some input sequence if no other

strategy would have satisﬁed it in the same situation. Thus, remorsefree dominance is a

weaker requirement than winning and therefore individual dominant strategies exist for more

systems. Formally, remorsefree dominant strategies are deﬁned as follows:

IDeﬁnition 1

(Dominant Strategy [

])

Let

be an LTL formula. Let

and

be strategies

for process

. Then,

is dominated by

, denoted

ts

, if for all input sequences

γ∈

)

either

comp

(

s, γ

)

comp

(

t, γ

)

holds. Strategy

is called dominant for

ts

holds for all strategies tfor process pi.

Intuitively, a strategy

dominates a strategy

if it is at least as good as

. It is dominant

for

if it is at least as good as every other possible strategy and thus if it is as good as

possible. As an example, reconsider the message sending system. Let

be a strategy for

process

that outputs

in the very ﬁrst step. It satisﬁes

m1∧m2

on all input

sequences containing at least one

m3−i

. On all other input sequences, it violates

. Let

be some alternative strategy. Since no strategy for

can inﬂuence

m3−i

satisﬁes

only

on input sequences containing at least one

m3−i

. Yet,

satisﬁes

for such sequences as

well. Hence, sidominates tiand since we chose tiarbitrarily, siis dominant for ϕ.

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

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

10 玖币 0人已下载

立即下载

摘要：

SynthesizingDominantStrategiesforLiveness(FullVersion)BerndFinkbeiner!CISPAHelmholtzCenterforInformationSecurity,Saarbrücken,GermanyNoemiPassing!CISPAHelmholtzCenterforInformationSecurity,Saarbrücken,GermanyAbstractReactivesynthesisautomaticallyderivesastrategythatsatisesagivenspecication.However,...

展开>> 收起<<

Synthesizing Dominant Strategies for Liveness Full Version.pdf

共33页,预览5页

还剩页未读，继续阅读

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

Synthesizing Dominant Strategies for Liveness Full Version

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: