AI帮你理解科学

AI 生成解读视频

AI抽取解析论文重点内容自动生成视频


pub
生成解读视频

AI 溯源

AI解析本论文相关学术脉络


Master Reading Tree
生成 溯源树

AI 精读

AI抽取本论文的概要总结


微博一下
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

被引用665|浏览22
EI
下载 PDF 全文
引用
微博一下

摘要

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...更多

代码

数据

简介
  • 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
您的评分 :
0

 

标签
评论
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科