We study fl3e expressive power of temporal logics obtained by extending or restricting UB
Decision procedures and expressiveness in the temporal logic of branching time
STOC, no. 1 (1985): 1-24
We consider the computation tree logic (CTL) proposed in ( Sci. Comput. Programming 2 (1982), 241–260) which extends the unified branching time logic (UB) of (“Proc. Ann. ACM Sympos. Principles of Programming Languages, 1981,” pp. 164–176) by adding an until operator. It is established that CTL has the small model property by showing that...更多
下载 PDF 全文
- Abstr(.cl: In this paper the authors consider tile Col]q)Uhlti~ii Tree l.ogic (CTI.) proposed in [CF.] which e:,tct!ds the Unified Ihandting Time logic (UI0 ~f [BMP] by adding an uutil operator.
- The authors can view a structure as a labelled directed graph whose nodes are the states.
- 2.5 I}efinition: A state formula p is satisfiable iff for some model M = (S,I.,R) and some s E S, M,s I= p.
- Abstr(.cl: In this paper we consider tile Col]q)Uhlti~ii Tree l.ogic (CTI.) proposed in [CF.] which e:,tct!ds the Unified Ihandting Time logic (UI0 ~f [BMP] by adding an uutil operator
- If we extend the syntax to allow,~';sertions such as E[l:p A Gq] ("for some computation path, there is a state on the path where p holds and for all states on that same path, q holds") where a path quantifier is paired with a Boolean combination of state quantifiers, we obtain the language we call UB +
- UP, is obtail;ed by restricting the UB syntax to allow only the pairs EX and EF (AG and AX can be obtained by negation) and corresponds to the nexttime logic of Manna and Pnueli [MP]. We show that these kmguages o m be arranged in the following hierarchy of expres:,ive power: UB- < UII < UB + < CTL _= CTL +
- We show how to use these DAGs to c(mstruct for each node s of M, a fiagment FRAG[s] such that every eventuality fommla in l.(s) is fulfilled within FRAG[s]
- Mj+ l is obtained by extending the frontier of Mj as follows: Ifqj+ t is fulfilled for s in Mj, let Mj+ 1 = Mj
- Once we have shown this, we can argue as follows: It is easy to check by propositional reasoning that for any q £ FL(P0 ) we have
- Lbrmula p, if M is a model for p, M/~i..14p) is a tlintikka structure for 13 with the property that satisfiability is preserved fi?r formulas in Fl.(p); i,e.
- The authors need the following definition: 4.2 I)efiuitio,: Let M be a structure, s a state in M, and p ( L ( s ) where p is an eventuality fommla, i.e. p is of the form EFq, AFq, E[q' U q], or A[q' U q].
- 4.,4 Lemma: I.et M be a psendo-Hintikka structure of size N0, s a state of M, and p an eventuality formula in l.(s).
- In the proof of tile Dllowing lenmm the authors explain how to construct FRAGs fi'om DAGs. 4.5 Lemma: Suppose s is a state in a pseudo-llinfikka structure M of size N0.
- Mj+ l is obtained by extending the frontier of Mj as follows: Ifqj+ t is fulfilled for s in Mj, let Mj+ 1 = Mj. Otherwise, suppose qj+l is of the form EFq. by Lemma 4.3, there is a frontier node t of Mj, with
- Let Mj+ 1 be the result of replacing each tii by DAG[ti, AFq] and again identifying any frontier nodes with the same labels.
- By Ax5 it follows that AXp A EX-~p, and Ps A EXp,, is inconsistent The proof in the other case is similar.
- A similar argument shows that if EFp 6 s and s is eliminated at step 4 because }t17 is not satisfied, Ps is inconsistent.
- As in 5.1, if there is a state containing P0 wlfich is not eliminated, the authors have constructed a pseudo-llintikka structure for P0, so P0 is satisfiable.
- Mi+ 1, si I==q iff Mi, si ~ q iff N i, si ~ q iff Ni+ 1, sl I==q) Ifp is of the fonn EGq. Mi+ 1, si+ 1 I=: EGq iff there is a path in Mi+ 1 startitlg at si+ 1 all ofwhose nodes satisfy q iff Mi+ 1, %+1 I=: q and Mi+ 1, tit- l I==q (by (2)above) iff Ni+ l, si+ 11==q arid Ni+ 1, ti+ l I-= qothesis) iff Ni+ l, si+ 1 I= EGq. suppose p is of the Ibrm EFq and Mi+l, %+1 I= El:q.
- 'lqm first author was partially supported by NSF Grant NICS79-08365
- The second author was partially supported by NSF Grant b1CS8010707 and a grant from tile National Science and I:ngineering Research Council of Canada