BRICS Basic Research in Computer Science

BRICS R S-99-32 Aceto & L ar oussinie: Is y o ur Model C heck er on T ime?

BRICS

Basic Research in Computer Science

Is your Model Checker on Time?

On the Complexity of Model Checking for Timed Modal Logics

Luca Aceto

Franc¸ois Laroussinie

BRICS Report Series RS-99-32

ISSN 0909-0878 October 1999

Copyright c 1999, Luca Aceto & Franc¸ois Laroussinie.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications.

Copies may be obtained by contacting:

BRICS

Department of Computer Science University of Aarhus

Ny Munkegade, building 540 DK–8000 Aarhus C

Denmark

Telephone: +45 8942 3360 Telefax: +45 8942 3255 Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk ftp://ftp.brics.dk

This document in subdirectory RS/99/32/

OntheComplexity ofModelCheckingforTimedModalLogics

LucaAceto

1

andFrançoisLaroussinie

2

1

BRICS

? ? ?

,DepartmentofComputerScience,AalborgUniversity,

FredrikBajersVej7-E,DK-9220AalborgØ,Denmark.

Email:luca@cs.auc.dk, Fax:+4598159889

2

LaboratoireSpécication etVérication,CNRSUMR8643,

ENSdeCachan,61av.duPr.Wilson,94235 Cachan,France.

Email:fl@lsv.ens-cachan.fr,Fax:+33147402464

Abstract. Thispaperstudiesthestructuralcomplexityofmodelcheck-

ingfor(variationson)thespecicationformalismsusedinthetoolsCMC

andUppaal, and fragmentsof atimedalternation-free

µ

^{-calculus.For}

eachofthelogicswestudy,wecharacterizethecomputationalcomplexity

ofmodelchecking,as wellas itsspecication and programcomplexity,

usingtimedautomataasoursystemmodel.

1 Introduction

Theextensionofthemodelcheckingparadigmtothespecicationandverica-

tionofreal-timesystemshasbeenthoroughlystudiedinthelastfewyears.This

extensiveresearcheorthasled to thedevelopmentof specicationlogics that

extend standard untimed formalisms with the quantitative analysis of timing

constraints(see,e.g.,[4,15,18]),andtoimportanttheoreticalresultssettingthe

limitsof decidabilityformodelchecking.This theoryis now embodied in veri-

cation toolslikeHyTech [23],Kronos[24] and Uppaal[20],which havebeen

successfullyappliedto thevericationofrealsizedsystems.

The successful application of the aforementioned verication tools to the

analysis of realistic systems indicates that automatic verication of real-time,

embedded software may be feasiblein practice.However, despitemanyimpor-

tant theoreticalresultspresentedin op.cit.,theliteratureis lackingacompre-

hensive analysis of the structural complexity of model checking for real-time

logics.Intheuntimedcase, modelcheckingalgorithmswith apolynomialtime

complexity,andoftensmallspacerequirements,havebeendevelopedforseveral

branchingtimetemporallogics[8,9].Inthetimedcase,mostofthemodelcheck-

ing problems considered in theliterature are PSPACE-hard [3,10,15]. Clearly

thequantitativeanalysisoftimingconstraintsincreasesthecomplexityofmodel

checking,butitisinterestingtoanalyzepreciselyinwhichcasesthiscomplexity

blow-upoccurs.Intheuntimedcase,severalpapers(see,e.g.,[13,22,11])study

indetailtheeectofthetemporaloperators,thenumberofatomicpropositions

? ? ?

BasicResearchinComputerScience.

a better understanding of the complexity issue. Here,among other things, we

addressthe samekind of problem for thetimed case:what happensif time is

insertedeither onlyin themodel oronlyin theformula?Andwhat happensif

weuselessexpressivelogicswithrestrictedoperators?

Weconsiderseveraltimedmodallogics:L

ν

^{hasbeenintroducedin[18],andis}

thespecicationlanguageusedinthetoolCMC[17];

L s

^{isafragmentofL}

ν

^which

hasbeenproposedin[19]inordertoimprovetheeciencyofmodelcheckingin

practice;SBLL[2] and

L _∀ S

^{[1] havebeenintroducedfor theirpropertiesw.r.t.}

thetestingtimedautomatonmethodthat iscurrentlyusedinvericationtools

likeUppaaltocheckforpropertiesotherthanplainreachabilityones.

Foreachofthesepropertylanguages,westudythecomputationalcomplexity

ofmodelchecking,usingtimedautomata[5]asoursystemmodel.Asarguedby

LichtensteinandPnueli[21],thecomplexityofthemodelcheckingproblemcan

bemeasuredinthreedierentways.First,onecanxthespecicationandmea-

surethecomplexityasafunction of thesize oftheprogrambeingveried(the

programcomplexitymeasure). Secondly, onecanxthe programand measure

the complexity as afunction of the size of the specication (the specication

complexity measure). Finally, the combined complexity of the model checking

problemismeasuredasafunctionofthesizeofboththeprogramandthespec-

ication.Inthispaperweoercomplexityresultsforthesethreedierentviews

ofthemodelcheckingproblemforthelogicsweconsider.Insodoing,wegivean

a posteriori justication, couched in complexity-theoretic arguments, for some

of the folkbeliefs in the areaof model checkingfor real-time systems,and for

someofthechoicesmadebydevelopersofreal-timevericationtools.

Outline of the Main Results. We beginby analyzing the complexity of model

checking for L

µ,ν

^{, a timed} alternation-free modal

µ

^{-calculus (AFMC). In the}

untimed setting, such afragment of the modal

µ

^{-calculus plays an important}

roleasaspecicationformalismbecauseitisfairlyexpressiveanditsrestricted

syntaxmakesthesymbolicevaluationofexpressionsverysimple(moreprecisely,

linearbothinthesizeofthemodelandthespecication).Inthereal-timesetting,

weshowthatthecomplexityofmodelcheckingforthetimedAFMC,andforits

sublogicL

ν

^,isEXPTIME-complete,asareboththeprogramcomplexityandthe specicationcomplexity.(Perhapssurprisingly,themodelcheckingproblemfor

L

ν

^{andafortioriforthetimedAFMCis} EXPTIME-complete evenifwex

themodeltobetheinactiveprocesswithoutclocks,

nil

^{.)Wealsoprovethatthe}

model checking problemfor L

ν

^{withoutgreatest}xpointsessentially, atimed versionofHennessy-Milnerlogic[14]isPSPACE-complete.

It isinstructiveto compare the aboveresultswith similar ones for theun-

timed alternation-free

µ

^{-calculus.Aspreviouslymentioned,forsuchaprogram}

logic,wehavealgorithmsformodelcheckingthatrunintimelinearbothinthe

size of the program and of the specication. Moreover,boththe program and

the specication complexities are P-complete [6,12]. Note, however, that the

program complexity ofthe alternation-free

µ

^{-calculusfor concurrent programs}

is EXPTIME-complete [6],and this matchesexactlythecomplexity resultswe

L

µ,ν ,

^L

ν

EXPTIME-complete EXPTIME-completeEXPTIME-complete

L s , SBLL, L _∀ S

PSPACE-complete PSPACE-complete PSPACE-complete L

− ν

PSPACE-complete P PSPACE-complete

L ⁻ s

coNP-complete P coNP-complete

SBLL ⁻ , L ⁻ _{∀ S}

PSPACE-complete PSPACE-complete coNP-complete

Table1:OverviewoftheResults

oerfor L

µ,ν

^{modelchecking.It isalso} interestingtonote that thecomplexity of CTL model checkingand reachabilityfor concurrentprograms is PSPACE-

complete [6], matching the complexity of model checking for TCTL[4] and of

reachability in timed automata, respectively. These results seem to provide a

mathematical groundingto thefolk belief that clocks actlikeconcurrentpro-

grams,andthatincreasingthenumberofclockscorrespondstoaddingparallel

components.

Wethen proceedtodevelopathoroughanalysisof thecomplexityofmodel

checkingforall theother timed modal property languagesthat wehavefound

in the literature. In each case, we oer results pinpointing the program, the

specicationaswellasthecombinedcomplexityofmodelcheckingfortheprop-

erty languageswith and withoutxpoints.An overviewof theresults wehave

obtainedis presentedin Table1, where

L ⁻

^{denotes thexpointfree fragment}

of

L

^{. Here wejust wish to point outthat the model checkingproblem for the}

propertylanguage

L s

^isPSPACE-complete,nomatterwhetherthecomplexityis measuredwithrespecttothesizeoftheprogram,ofthespecicationorofboth.

Inlight ofthe aforementionedresults,and assumingthat PSPACE is dierent

fromEXPTIME, themodelcheckingproblemfor

L s

^hasalowercomputational complexitythanthat forL

ν

^{.Ourresultsthusoera}complexity-theoreticjusti- cation fortheclaims in [19].Thesourceof thelowercomplexityderivesfrom

theobservationthatthemodelcheckingproblemfor

L s

^{,unlikethatforL}

ν

^,can

be reducedin polynomial time to reachabilitycheckingin timed automataa

problemwhosePSPACE-completenesswasshownin [5].

2 Basic denitions

We begin bybriey reviewinga variationonthe timed automatonmodel pro-

posedbyAlurandDill[5]andthepropertylanguagesthatwillbeusedin this

study.

TimedAutomata. Let Act be anite set ofactions,and let

N

^and

R ≥ 0

^denote

thesetsofnaturalandnon-negativerealnumbers,respectively.Wewrite

D

^for

thesetofdelayactions

{ (d) | d ∈ R ≥ 0 }

^.

Let

C

^{beasetofclocks.Weuse}

B (C)

^{todenotethesetofboolean}expressions overatomic formulaeof theform

x ∼ p

^and

x − y ∼ p

^{, with}

x, y ∈ C

^,

p ∈ N

^,

and

∼∈ {<, >, =}

^{. Moreover we write}

B k (C)

^{for the} restriction of

B(C)

^to

expressions where the integer constants belong to

{0, . . . , k}

^. Expressions in

B(C)

^areinterpretedoverthecollectionoftimeassignments.Atimeassignment,

orvaluation,

v

^for

C

^{isafunctionfrom}

C

^to

R ≥ 0

^.Wewrite

R ^C _≥ 0

^{forthecollection}

ofvaluationsfor

C

^.Given

g ∈ B (C)

^{andatimeassignment}

v

^{,thebooleanvalue}

g(v)

^{describes whether}

g

^{is satisedby}

v

^{or not.Foreverytime assignment}

v

and

d ∈ R _≥ 0

^,weuse

v + d

^{todenotethetimeassignmentwhichmapseachclock}

x ∈ C

^tothevalue

v(x) +d

^.Forevery

C ⁰ ⊆ C

^,

[C ⁰ → 0]v

^{denotestheassignment}

for

C

^{whichmaps eachclockin}

C ⁰

^{to thevalue}

0

^{andagreeswith}

v

^over

C\C ⁰

^.

Denition1. A timed automaton(TA) isa quintuple

A = h

^Act

, N, n 0 , C, Ei

where

N

^{isanitesetofnodes,}

n 0

^{istheinitialnode,}

C

^{isanitesetofclocks,}

and

E ⊆ N×B(C)×

^Act

×2 ^C ×N

^{isasetofedges.Thetuple}

e = hn, g, a, r, n ⁰ i ∈ E

stands for an edge from node

n

^{to node}

n ⁰

^{with action}

a

^{, where}

r

^{denotes the}

setof clocks tobereset to

0

^and

g

^{isthe enabling condition(orguard). Weuse}

MCst

(A)

^{todenotethe largestintegerconstantoccurring inthe guardsof}

A

^.

A state(or conguration)of atimed automaton

A

^{is apair}

(n, v)

^where

n

^isa

nodeof

A

^and

v

^{isatimeassignmentfor}

C

^{.Theinitialstateof}

A

^is

(n 0 , [C → 0])

where

n 0

^{istheinitialnode of}

A

^{, and}

[C → 0]

^{isthetimeassignmentmapping}

allclocksin

C

^to

0

^.Theoperationalsemanticsofatimedautomaton

A

^isgiven

bytheTimed LabelledTransitionSystem(TLTS)

T A = hS A ,

^Act

∪ D, s ⁰ , −→i

^,

where

S A

^{is the set of statesof}

A

^,

s ⁰

^{is theinitial stateof}

A

^{, and}

−→

^{is the}

transitionrelationdened asfollows:

(n, v) −→ ^a (n ⁰ , v ⁰ )

ⁱ

∃hn, g, a, r, n ⁰ i ∈ E. g(v) = tt ∧ v ⁰ = [r → 0]v (n, v) −→ ^(d) (n ⁰ , v ⁰ )

ⁱ

n = n ⁰

^and

v ⁰ = v + d

Remark 1. NotethatwecouldconsiderextendedTAswhereweassignaninvari-

ant(i.e.adownwardclosedclockconstraint)toeachnodetoavoidexcessivetime

delays.AlltheresultspresentedherewillstillholdforextendedTAs.Notethat,

givenacomplexityclass

C

^,havinga

C

^{-hardnessresultfor(simple)TAsimplies}

the samefor extended TAs, while havinga

C

^{membership resultfor extended}

TAsimpliesthesameforTAs.

Thespecication languages. WenowdeneL

µ,ν

^atimedalternation-freemodal

µ

^-calculus.

Denition2. Let

K

^{beanitesetofclocks,Idasetofidentiers.ThesetL}

µ,ν

of formulaeover

K

^{andId isgeneratedbythe followinggrammar:}

L

µ,ν 3 ψ , ϕ ::= g | ϕ ∧ ψ | ϕ ∨ ψ | hai ϕ | [a] ϕ | ∃∃ϕ | ∀∀ϕ

| K ⁰

ⁱⁿ

ϕ |

^max

(X, ϕ) |

^min

(X, ϕ) | X

where

a ∈

^Act,

g ∈ B(K)

^,

K ⁰ ⊆ K

^and

X ∈

^{Id. Moreover, each occurrence}

of an identier

X

^{ina formula has tobe boundby a min}

(X, ϕ)

^{(or max}

(X, ϕ)

⁾

operator, and it cannot occur in a

ϕ

-subformula of the form max

(X ⁰ , ψ )

^(resp.

min

(X ⁰ , ψ )

^).(This restriction correspondstothe alternation-free property.)

New operators like

tt

^,

ff

^,

g ⇒ ψ

^{(read `}

g

^implies

ψ

^{') can be easily dened.}

LetMCst

(ϕ)

^{bethelargestintegerconstantoccurringintheclock}constraintsin

ϕ

^{. Given aTA}

A

^{, weinterpretformulaein L}

µ,ν

^{w.r.t.extended} congurations

(n, v, u) | = [a] ϕ

ⁱ

∀ (n ⁰ , v ⁰ ). (n, v) −→ ^a (n ⁰ , v ⁰ ) ⇒ (n ⁰ , v ⁰ , u) | = ϕ (n, v, u) | = ∀∀ ϕ

ⁱ

∀ d ∈ R ≥ 0 , (n, v + d, u + d) | = ϕ

(n, v, u) | = g

ⁱ

g(u) = tt

(n, v, u) | = K ⁰

ⁱⁿ

ϕ

ⁱ

(n, v, [K ⁰ → 0]u) | = ϕ

(n, v, u) | =

^max

(X, ϕ)

ⁱ

(n, v, u)

^{belongstothelargestsolutionof}

X = ϕ

Table2:SemanticsofL

µ,ν

^.

(n, v, u)

^{, where}

(n, v)

^{is a}congurationof

A

^and

u

^{isatime assignmentfor}

K

^.

Whereastheclassicalmodaloperators

hai

^and

[a]

^{dealwithaction}transitions, theoperator

∃∃

^(resp.

∀∀

^)denotesexistential(resp.universal)quanticationover delay transitions. The clocks in

K

^{are so-called formula clocks; they increase}

synchronouslywiththe automataclocks, andthey areused asstopwatchesfor

measuringthetimeelapsingbetweenstatesofthesystem.Theformula

K ⁰

ⁱⁿ

ϕ

initializestheset offormulaclocks

K ⁰

^to

0

ⁱⁿ

ϕ

^.Theconstraints

g

^{areused to}

comparethevalueofformulaclocksin thecurrentextendedcongurationwith

an integer value. Finally, an extended conguration satises max

(Z, ϕ)

^(resp.

(

^min

(Z, ϕ)

^{) if it belongs to the largest (resp. least) solution of the equation}

Z = ϕ

^{overthecompletelatticeofsetsofextended}congurations.Theexistence of these solutions is guaranteed by standardxpoint theory. The semanticsof

L

µ,ν

^{is sketched in Table2.(The operators}

hai

^and

∃∃

^{are dualsof}

[a]

^and

∀∀

^;

the semanticsof boolean operators is omitted.) The full formal details of the

semanticsarestandard[16].

As anexample of aproperty that can be expressed in L

µ,ν

^{using xpoints}

andclockconstraints,consider theformula

max

X,

[b]{x}

ⁱⁿ

∃∃(hci tt ∧ x ≤ 3)

∧ [a]X ∧ ∀∀X .

This formula expresses the fact that, in everystate that is reachable by per-

forming

a

^{-actionsanddelays,everyoccurrenceofa}

b

^{-actioncanbefollowedby}

a

c

^{-actionwithin}

3

^timeunits.

Fragments of L

µ,ν

^{. The logic L}

ν

^{[18] is the fragment of L}

µ,ν

^{in which only}

greatest xpointsare allowed.The logic

L s [19]

^{isthe fragment of L}

ν

^without

theexistentialmodalities

hai

^and

∃∃

^{, andwhereonlyarestricted}disjunctionof theform

g ∨ ϕ

^(with

g ∈ B(K)

^)isallowed.

Thepropertylanguages

SBLL

^and

L _∀ S

^extend

L s

^{, anduseaslightlydierent}

kindofTAswhere(1)

U

^{isasubsetofActs.t.anyedgelabeledwith}

a ∈ U

^hasthe

guard

tt

^{and(2)Actcontainsthelabel}

τ

^{usedfortheinternalactionofautomata.}

Moreovertheyare basedondierent semantics(denoted by

`

^{)compared with}

L

ν

^and

L s

^{: a formula}

ϕ

^{holds for}

(n, v, u)

^{only if}

ϕ

^{holds for every}

(n ⁰ , v ⁰ , u)

with

(n ⁰ , v ⁰ )

^{reachablefrom}

(n, v)

^{in zero or more}

τ

-transitions. Forexample,

(n, v, u) ` [a]ϕ

^iforevery

(n, v) −→ ^{τ ∗} (n ⁰ , v ⁰ )

^wehavethat

(n ⁰ , v ⁰ ) −→ ^a (n ⁰⁰ , v ⁰⁰ )

implies

(n ⁰⁰ , v ⁰⁰ , u) ` ϕ

^.Moreover

(n, v, u) ` ∀∀ϕ

^iforevery

(n ⁰ , v ⁰ )

^reachedfrom

(n, v)

^byusing

τ

-transitionsanddelaytransitions(oftotalduration

d

^),wehave

(n ⁰ , v ⁰ , u + d) ` ϕ

^.

SBLL

^extends

L s

^{by allowing the useof}

hai tt

subformulae with

a ∈ U

^.

L _∀ S

extends

SBLL

^{with new operators}

∀∀ S

^with

S ⊆ U

^{. A formula}

∀∀ S ϕ

^{holds for}

(n, v, u)

ⁱ

ϕ

^{holds forany}

(n ⁰ , v ⁰ , u + d)

^s.t.

(n ⁰ , v ⁰ )

^{is reachablefrom}

(n, v)

^by

usingonly

τ

-transitionsanddelaytransitions(withtotalduration

d

^),butdelay

transitionsoccuronlyin statesin whichnoneoftheactionsin

S

^areenabled.

These two languagescanbe translated into L

ν

^{in the following sense: for any}

ϕ ∈ L _∀ S

^{, there exists an L}

ν

^formula

ϕ

^s.t.

A ` ϕ

ⁱ

A | = ϕ

^{. Forexample, we}

have that

[a]ψ =

^max

(X, [a]ψ ∧ [τ]X )

^{. An important property [2,1] of}

SBLL

and

L _∀ S

^{is thattheirmodel checkingproblem canbereducedtoa}reachability problem:foranyformula

ϕ

^{oftheselanguages,wecanbuildatestingautomaton}

T ϕ

^s.t.

A ` ϕ

^{i a reject node is not reachable in the parallel} composition

(A|T ϕ )

^{. Moreover it has beenshown that}

L _∀ S

^{is expressiveenough to encode}

anyreachabilityproperty[1].

Verication oftimedsystems. Automaticvericationoftimedsystemsispossi-

bledespitetheuncountablyinnitenumberofcongurationsassociatedwitha

timedautomaton.Thedecisionprocedurefor

A | = ϕ

^{isbasedonthewellknown}

region technique [4]. Given

A

^and

ϕ

^{, it is possibleto partition the innite set}

oftimeassignmentsover

C ⁺ = C ∪ K

^{into anitenumberofregionsin sucha}

waythattwoextendedcongurations

(n, u)

^and

(n, v)

^,where

u, v ∈ R ^C _≥ ⁺ 0

^arein

thesameregion,satisfythesameformulae.Formallytheregionscanbedened

as the equivalence classes induced by the equivalence relation over valuations

dened thus: given

u, v ∈ R ^C _≥ ⁺ 0

^,

u

^and

v

^{are in the sameregioni theysatisfy}

thesameclockconstraintsin

B M (C ⁺ )

^,where

M = max(

^MCst

(A),

^MCst

(ϕ))

^.

Wewrite

[u]

^{fortheregionwhichcontainsthetimeassignment}

u

^,anduse

R ^Cl k

to denotethe(nite)set ofallregionsforaset

Cl

^{of clocksandthemaximum}

constant

k

^{.Givenaregion}

[u]

ⁱⁿ

R ^Cl _k

^and

C ⁰ ⊆ Cl

^{,wedenetheresetoperator}

thus:

[C ⁰ → 0][u] = [[C ⁰ → 0]u]

^{.Moreover,givenaregion}

γ

^{,itssuccessorregion,}

denotedby

succ(γ)

^,istheregion

γ ⁰

^s.t.forany

u ∈ γ

^{there exists}

δ ∈ R _≥ 0

^with

[u+δ] = γ ⁰

^,and

[u+δ ⁰ ] ∈ {γ, γ ⁰ }

^,forevery

δ ⁰ < δ

^.Theregion

succ(γ)

^isdierent

from

γ

ⁱ

γ(x ≤ k) = tt

^forsomeclock

x

^.

Now, given a timed automaton

A = h

^Act

, N, n 0 , C, Ei

^{, a set}

K

^{of formula}

clocks and an integer constant

M

^with

M ≥

^MCst

(A)

^{, we can dene a sym-}

bolicsemantics[18]overthenitetransitionsystem

(S, →)

^{,calledregiongraph,}

dened thus:

S = N × R ^C M ^{∪ K}

^and

→= ( S

a

−→)∪ a −→ ^succ

^{. The symbolic se-}

mantics is closely related to the standard one: for every L

µ,ν

^{formula whose}

clock constraints donotuse constantsgreater than

M

^{, and}

u ∈ γ

^,

(n, γ) | = ϕ

i

(n, u) | = ϕ

^{. Therefore each instance of the timed model checking problem}

can be reduced to an untimed model checking query over the region graph.

Note that the size of

R ^C M ⁺

^{is in}

O(|C ⁺ |! · M ^{| C + |} )

^{. Moreover for any region}

γ

^,

|{γ ⁰ |γ ⁰ = succ ⁱ (γ), i ∈ N}| ≤ 2 · |C ⁺ | · (M + 1)

^.

Thereachabilityproblem,whichisafundamentalquestioninsystemverication,

isknowtobePSPACE-complete [3,10]. Moreoverthemodelcheckingproblem

forTCTL(atimedextensionofCTL)isPSPACE-complete[4].

We shall use the abbreviations

A +t | =

^?

Ψ +t

^,

A | =

^?

Ψ +t

^and

A +t | =

^?

Ψ

^to

denote,respectively,themodelcheckingproblemswhereclocksareallowedboth

andwhereclocksareallowedonlyinautomata.

3 Complexity results for model checking

Wenowconsiderthe complexityofmodelchecking(MC)forthepropertylan-

guagesintroducedpreviously.Theseresultsrequiretodenewhatarethesizeof

atimedautomaton

A = h

^Act

, N, n 0 , C, Ei

^andaformula

ϕ ∈

^L

µ,ν

^{. Thesize}

|ϕ|

ofaformulaisitslength.Wedene

|A|

^as

|N| + |C| + |E| +

^MCst

(A) + Σ e ∈ E |g e |

^,

andassumeabinaryencodingfortheelementsofthesets

N

^and

C

^.Consider-

ingconstantsrepresentedinunaryorbinarydoesnotchangeourresultsexcept

whenitisexplicitlymentioned.

Theorem 1. The complexity of L

µ,ν

^{and L}

ν

^{model checking is EXPTIME-}

complete. Moreover, we have that the specication andprogram complexities of

L

µ,ν

^andL

ν

^{model checking arealso}EXPTIME-complete.

Proof. EXPTIME membership:Wehaveseenthat

A | = ϕ

ⁱ

A ˜ | = ϕ

^where

A ˜

^{isan untimedautomaton (the region graph) whose sizeis} exponentialin

| A |

andoverwhich

ϕ

^isinterpretedasanuntimed formula.Ifwemodifyslightly

A ˜

by adding the transitiveclosure of

succ −→

^{, the size of the resultingautomaton is}

stillexponentialin

|A|

^,and

∃∃

^and

∀∀

^{becomeonestep} modalities.Then

ϕ

^isa

simple(untimed) alternation-free

µ

^{-calculus formulafor which model checking}

is linearin

| A| ˜

^and

|ϕ|

^{[9].This givestheEXPTIME membershipfor L}

µ,ν

^and

L

ν

^.

EXPTIME-hardness: Deciding whether a given linear bounded alternating

Turing machine (LBATM)

M

^{accepts a given input string}

w

^{is EXPTIME-}

complete[7],anditcanbereducedinpolynomialtimetoaMCproblem

A _M | = Φ

with

Φ ∈

^L

ν

^{.The mainideais that wecanbuildaTA}

A _M

^overactions

s

^and

accept s.t. any

s

-transition of

A _M

corresponds to a step of

M

^{due to the}

tapeboundness(see[3,10]).Byfollowingthesameapproachproposedin [6]for

untimedconcurrentsystems,thealternatingbehaviour 1

of

M

^{canbehandledby}

anL

ν

^{formulaoftheform:}

Φ =

^max

(X, [

^accept

]ff ∧ ∀∀ [s] ∃∃ h s i X )

^.Intuitively

Φ

holdsfor

A _M

^{ifthecurrentorstateisnotanacceptingstateandafteranystep}

(leading toanand state),there existsatransition leadingto anon-accepting

or stateand soon.We have

A _M | = Φ

^{i theLBATM}

M

^{doesnot accept}

w

^.

ThisgivestheEXPTIME-hardnessforL

ν

^andL

µ,ν

^.

Specicationcomplexity:Infacttheacceptanceof

w

^byaLBATM

M

^canbe

reducedinpolynomialtimetoaproblemoftheform

nil | = Ψ _M ,w

^where

Ψ _M ,w

^is

anL

ν

^{formula.Thisencodingisbasedontheuseofformulaclockstorepresent}

thecongurationsof

M

^{.Thisgivesthe}EXPTIME-hardness.

Program complexity:Thisis duetotheproofofEXPTIME-hardnessforL

ν

model checkingwhere theformula

Φ =

^max

(X, [

^accept

]ff ∧ ∀∀ [s] ∃∃ hsi X )

^does

notdepend ontheLBATM

M

^{. 2}

1

Weassumew.l.o.g.thatwehaveastrictalternationofor andandstatesin

M

^,

andthattheinitialandnalstatesareorstates.

sat t = 1 a 1 x 1 := 0 t = 2 a 2 x 2 := 0 t = n a n x n := 0

r _n r 1

r 0

t = 1 a 1 t = 2 a 2 t = n a n

t = n ∧ ϕ ˜ end

Fig.1:Theautomaton

A (ϕ)

^with

ϕ ˜ = ϕ[p i ← x i = n − i; ¯ p i ← x i = n]

^.

Remark 2. In[15],atimed

µ

^-calculus

T µ

^{hasbeenproposed,andMCfor}

T µ

^was

shownto be PSPACE-hard.

T µ

^{is moreexpressivethan L}

µ,ν

^{because itallows}

forxpointalternationsanditusesapowerfulbinaryoperator

.

^{(insteadofour}

modalities

hai

^and

∃∃

^{). Infact theproof of Theorem 1canbeadapted2 to}

T µ

andthisyieldsanimprovedlowerboundonthecomplexityof

T µ

^MC.Moreover,

using techniquesfrom [6], wecan provethat theMC problem for

T µ

^(andthe

extension of L

µ,ν

^with alternations) is in EXPTIME, and is thus EXPTIME- complete.Tothebest ofourknowledgethisistherstprecise characterization

ofthecomplexityofMCforthislogic.

Theorem2. The model checking problem for L

− ν

^isPSPACE-complete. More- overthe specication complexityof L

− ν

^{MC is}PSPACE-complete. The program complexity of L

− ν

^{MCis in P,if the integer constants inthe automata are rep-}

resentedinunary.

Proof. PSPACEmembership:Anondeterministicmodelcheckingalgorithm

in PSPACE canbeeasily dened by consideringthe parts ofthe regiongraph

associatedto

A | = ϕ

^{onlywhentheyarerequired.ThedierencewithL}

ν

^isthat

wedonotneedto computearbitrarysetsofcongurationsforxpoints.

PSPACE-hardness: Let

Φ = Q 1 p 1 . . . Q n p n .ϕ

^{be an instance of the QBF}

(Quantied Boolean Formulae) problem, where each

Q i ∈ {∃, ∀}

^and

ϕ

^{is a}

propositional formula over the

p i

^{'s. We reduce the validity of}

Φ

^{to a model}

checkingproblem. ConsidertheTA

A (ϕ)

^{inFigure1andtheL}

−

ν

^formula

Φ ˜ = ∃∃(ha 1 i tt ∧ O 1 (∃∃(ha 2 i tt ∧ O 2 . . . ∃∃(ha n i tt ∧ O n hsati tt))))

where

O i

^is

ha i i

^(resp.

[a i ]

^)if

Q i

^is

∃

^(resp.

∀

^).Clearly

A (ϕ) | = ˜ Φ

ⁱ

Φ

^isvalid.

Specication complexity: In fact any QBF instance can be encoded as a

problemoftheform

nil | = Φ

^,with

Φ ∈

^L

⁻ ν

^{,byusingformulaclocks.Thisentails}

thePSPACE-hardnessofspecicationcomplexity.

Program complexity: Let

ϕ

^{be agiven L}

⁻ ν

^{formula. We candene a poly-}

nomial(in

| A |

^{) algorithmbybuildingthe pertinentpartof theregiongraphin}

an on the y manner. The keypointsare that (1) deciding if

ϕ

^{holds for a}

TA

A

^{needstoconsider onlysequenceswithat most}

| ϕ |

^actiontransitions and (2) betweentwo action transitions the number of possible delay transitions is

bounded by

2(|C A | + |K|)(max(

^MCst

(A),

^MCst

(ϕ)) + 1)

^{which is polynomialin}

|A|

^ifMCst

(A)

^{isgivenin unary.Thetimecomplexityofsuchanalgorithmisin}

O(|A| ^{2 | ϕ |} )

^and,as

ϕ

^{isxed,theprogramcomplexityisinP. 2}

2

Forex.byconsideringaformulalike:

µX.

^accept

∨ [tt. (p o ∧¬(tt .(p e ∧¬X )))]

^where

p e

^(resp.

p o

^{)markseven(resp.odd)states.}

lemsoftheform

nil | = ϕ

^(where

ϕ

^{isaformulainanyofthelogicsconsideredso}

far)arejust ashardastheMCproblemsforarbitraryTA. Thustheworst-case

complexityofMCforthesereal-timelogicsmaybeseenasderivingsolelyfrom

theuseofclocksinformulae.Thispatternwill remaintrueforalltheproperty

languageswestudy inwhatfollows,except

SBLL ⁻

^and

L ⁻ _{∀ S}

^.

Thepropertylanguage

L s

^{hasbeenintroducedin [19] asa}sub-languageof L

ν

^{that allowsformoreecientmodel checking}algorithms.Tothebest ofour knowledge, however, such an intention has not been supported yet by precise

complexitytheoreticconsiderations.Thesewenowproceedto present.

Theorem3. The complexity of

L s

^{MC is PSP}ACE-complete. Moreover, the specication andprogramcomplexitiesof

L s

^{MCarealso PSP}ACE-complete.

Proof. PSPACEmembership:Forevery

L s

^formula

ϕ

^{,itispossibletobuild}

aTA

T ϕ

^{suchthat,foranyTA}

A

^,

A | = ϕ

^{iarejectnodeof}

T ϕ

^{isnotreachable}

in theparallelcomposition

(A|T ϕ )

^{[2].Thesizeof}

T ϕ

^{islinearin that of}

ϕ

^and

(A|T ϕ )

^{can be seenasa newTA}

A ¯

corresponding to theproduct

A ×T ϕ

^{. The}

reductionof

A | = ϕ

^{to a}reachabilityproblemfor

A ¯

^{isdonein polynomialtime,}

andthusgivesthePSPACE membership.

PSPACE-hardness:A reachabilityquestionfor node

n

^{in aTA}

A

^canbere-

duced to checking that

A 6| =

^max

(X, [

^in_n

]ff ∧ [a]X ∧ ∀∀ X )

^{if wesuppose that}

everyedgein

A

^haslabel

a

^{,exceptforanewtransition}

h n, tt,

^in_n

, ∅ , n i

^.

Specication complexity: It is possible to reduce reachability in a linear

bounded nondeterministic Turing machine

M

^{with input}

w

^{to a problem of}

theform

nil | = Φ _M ,w

^{bymeansofthesamekindofencodingusedforL}

ν

^.

Programcomplexity:ItisPSPACE-completebecausetheformulaexpressing

thereachabilityproblemdoesnotdependontheinputautomaton. 2

Theorem4. The model checking problem for

L ⁻ _s

^is coNP-complete, as is the specication complexity of model checking. The program complexity of

L ⁻ _s

^isin

P,if the constantsin theinputautomataarerepresentedinunary.

Thepropertylanguages

SBLL

^and

L _∀ S

^havethesamecomplexity:

Theorem5. The complexity of

SBLL

^and

L _∀ S

^{model checking is PSPACE-}

complete. Moreover we have that the specication and program complexities of

SBLL

^and

L _∀ S

^{MCare also}PSPACE-complete.

Forthepropertylanguages

SBLL ⁻

^and

L ⁻ _{∀ S}

^{,weobtainthefollowingresult:}

Theorem6. TheMCproblemfor

SBLL ⁻

^and

L ⁻ _{∀ S}

^isPSPACE-complete. The specicationcomplexityofMCfor

SBLL ⁻

^and

L ⁻ _{∀ S}

^{iscoNP-hard,andiscoNP-}

completeifconstantsintheformulaearerepresentedinunary.Finally, the pro-

gramcomplexityof MCfor

SBLL ⁻

^and

L _∀ S

^isPSPACE-complete.

There isanimplicitrecursion(over

τ

^anddelaytransitions)whichishiddenin thesemanticsofthe

SBLL ⁻

^operator

∀∀

^{,andthisrecursionissucienttomake}

SBLL ⁻

^and

L ⁻ _{∀ S}

^{modelchecking}PSPACE-hard.

L

− ν

L _∀S

SBLL

L ⁻ s

L ⁻ _∀S

SBLL ⁻

PSPACE EXPTIME

coNP

L s

L

µ,ν

L

ν

L → L ⁰

^standsfor

"

L

^{ismoreexpressivethan}

L ⁰

^"

Fig.2:Expressivenessvscomplexityofmodelchecking

Concluding remarks. The relationships between the relative expressive power

ofthepropertylanguagesthatwehaveconsidered,andthecomplexityoftheir

model checking problems is summarized in Figure 2. (There

L −→ L ⁰

^means

that anymodel checkingproblem

A | = ϕ

^with

ϕ ∈ L ⁰

^{canbereducedin linear}

timeto averication

A ˜ | = ˜ ϕ

^with

ϕ ˜ ∈ L

^.)

Note that, for every specication language we consider, the proof of

C

^-

hardness of the MC problem uses formulae without clocks. This implies that

theproblems

A +t | =

^?

Ψ

^and

A +t | =

^?

Ψ +t

^{havethe same}complexity. Theremark aboutthecomplexityofMCproblemsoftheform

nil | = ϕ

^showsthat

A | =

^?

Ψ +t

and

A +t | =

^?

Ψ +t

^{alsohavethesamecomplexity.ThereforethecomplexityofMC}

doesnotdependonwhether timeisaddedtothemodel,to thespecicationor

toboth.

References

1. L.Aceto,P.Bouyer,A.Burgueño,andK.G.Larsen,Thepowerofreach-

abilitytestingfortimedautomata,inProc.ofFSTTCS'98,LNCS1530,December

1998,pp.245256.

2. L. Aceto, A. Burgueño, and K. G. Larsen, Model checking viareachabil-

ity testing for timed automata, inProc. ofTACAS '98, LNCS1384, April1998,

pp.263280.

3. R.Alur,TechniquesforAutomaticVericationofReal-timeSystems,PhDthesis,

StanfordUniversity,1991.

4. R. Alur, C. Courcoubetis,and D. Dill, Model-checking in densereal-time,

InformationandComputation,104(1993),pp.234.

5. R. Alurand D. Dill, A theory of timedautomata,Theoretical ComputerSci-

ence,126(1994),pp.183235.

6. O.Bernholtz,M.Y.Vardi,andP.Wolper,Anautomata-theoretic approach

tobranching-timemodelchecking,inProc.ofthe6th.InternationalConferenceon

Computer-Aided Verication, CAV'94, D. Dill, ed., vol. 818of LectureNotes in

ComputerScience,California,USA,June1994,Stanford,Springer-Verlag.

7. A.K.Chandra,D.C. Kozen,andL.J.Stockmeyer,Alternation,J.Assoc.

Comput.Mach.,28(1981),pp.114133.

nitestateconcurrentsystem usingtemporallogic,ACMTrans.onProgramming

LanguagesandSystems,8(1986),pp.244263.

9. R. Cleaveland,A linear-time model-checking algorithm forthe alternation-free

modal

µ

^{-calculus,FormalMethodsinSystemsDesign,2(1993),pp.121147.}

10. C.CourcoubetisandM.Yannakakis,Minimumandmaximumdelayproblems

inreal-timesystems,FormalMethodsinSystemDesign,(1992),pp.385415.

11. S.Demri andP.Schnoebelen,Thecomplexityofpropositionallineartemporal

logics in simple cases (extended abstract), inProc. 15thAnn.Symp.Theoretical

Aspectsof ComputerScience(STACS'98), LNCS1373,Paris, France,Feb.1998,

SpringerVerlag,1998,pp.6172.

12. S.Dziembowski,M.Jurdzi«ski,andD.Niwi«ski,Ontheexpressioncomplex-

ity of the modal

µ

^{-calculus model checking.} Unpublishedmanuscript, November 1996.

13. E. A.Emerson, C. S. Jutla,and A. P.Sistla,On model-checking forfrag-

mentsof

µ

^-calculus,inProceedingsoftheFifthInternationalConferenceComputer AidedVerication,Elounda,Greece, July1993, C.Courcoubetis, ed.,vol. 697of

LectureNotesinComputerScience,Springer-Verlag,1993,pp.385396.

14. M. Hennessy and R. Milner,Algebraiclaws for nondeterminism andconcur-

rency,J.Assoc.Comput.Mach., 32(1985),pp.137161.

15. T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model

checkingforreal-timesystems,InformationandComputation,111(1994),pp.193

244.

16. D.Kozen,Resultsonthepropositional

µ

^-calculus,TheoreticalComputerScience, 27(1983),pp.333354.

17. F. Laroussinie and K. G. Larsen, CMC: A tool for compositional model-

checking of real-time systems, inProc. IFIP Joint Int. Conf. FormalDescription

Techniques&ProtocolSpecication,Testing,andVerication(FORTE-PSTV'98),

KluwerAcademicPublishers,1998,pp.439456.

18. F. Laroussinie,K.G.Larsen,andC.Weise,Fromtimedautomatatologic-

andback,inProc.ofthe20th.InternationalSymposiumonMathematicalFounda-

tionsofComputerScience,MFCS'95,J.WiedermannandP.Hájek,eds.,vol.969of

LectureNotesinComputerScience,Prague,CzechRepublic,August28-Septem-

ber11995,Springer-Verlag,pp.529539.

19. K. G. Larsen, P. Pettersson,and W. Yi,Model-checking for real-time sys-

tems, in Proceedings of the 10th International Conference on Fundamentals of

Computation Theory, H. R. (Ed.), ed., Dresden, Germany,August 1995, LNCS

965,pp.6288.

20. ,UPPAALinaNutshell,JournalofSoftwareToolsforTechnologyTransfer,

1(1997),pp.134152.

21. O.LichtensteinandA.Pnueli,Checkingthatnitestateconcurrentprograms

satisfytheirlinearspecication,inConferenceRecordoftheTwelfthAnnualACM

Symposium on Principles of Programming Languages, New Orleans, Louisiana,

Jan.1985, pp.97107.

22. A.P.SistlaandE.M.Clarke,Thecomplexityofpropositionallineartemporal

logics,J.Assoc.Comput.Mach.,32(1985),pp.733749.

23. T.A.HenzingerandP.-H.Ho,andH.Wong-Toi,HyTech:AModelChecker

for HybridSystems, Journal ofSoftware Toolsfor Technology Transfer,1(1997),

pp.110122.

24. S.Yovine,Kronos:AVericationToolforreal-TimeSystems,JournalofSoftware

ToolsforTechnologyTransfer,1(1997),pp.123133.

Recent BRICS Report Series Publications

RS-99-32 Luca Aceto and Franc¸ois Laroussinie. Is your Model Checker on Time? — On the Complexity of Model Checking for Timed Modal Logics. October 1999. 11 pp. Appears in Kutyłowski, Pacholski and Wierzbicki, editors, Mathematical Foundations of Computer Science: 24th International Symposium, MFCS ’99 Proceedings, LNCS 1672, 1999, pages 125–136.

RS-99-31 Ulrich Kohlenbach. Foundational and Mathematical Uses of Higher Types. September 1999. 34 pp.

RS-99-30 Luca Aceto, Willem Jan Fokkink, and Chris Verhoef. Struc- tural Operational Semantics. September 1999. 128 pp. To ap- pear in Bergstra, Ponse and Smolka, editors, Handbook of Pro- cess Algebra, 1999.

RS-99-29 Søren Riis. A Complexity Gap for Tree-Resolution. September 1999. 33 pp.

RS-99-28 Thomas Troels Hildebrandt. A Fully Abstract Presheaf Seman- tics of SCCS with Finite Delay. September 1999. To appear in Category Theory and Computer Science: 8th International Con- ference, CTCS ’99 Proceedings, ENTCS, 1999.

RS-99-27 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Trans- forming Recursive Equations into Programs with Block Struc- ture. September 1999. 57 pp. To appear in the November 2000 issue of Theoretical Computer Science. This revised report su- persedes the earlier BRICS report RS-98-54.

RS-99-26 Jesper G. Henriksen. An Expressive Extension of TLC. Septem- ber 1999. 20 pp. To appear in Thiagarajan and Yap, editors, Fifth Asian Computing Science Conference, ASIAN ’99 Pro- ceedings, LNCS, 1999.

RS-99-25 Gerth Stølting Brodal and Christian N. S. Pedersen. Finding Maximal Quasiperiodicities in Strings. September 1999. 20 pp.

RS-99-24 Luca Aceto, Willem Jan Fokkink, and Chris Verhoef. Conser-

vative Extension in Structural Operational Semantics. Septem-

ber 1999. 23 pp. To appear in the Bulletin of the EATCS.