Computation tree logic: Difference between revisions

Revision as of 17:50, 15 March 2023

Revision as of 18:07, 15 March 2023

Line 28:

:<math>\mbox{EF }\big(r \mbox{ U } q\big)</math>

The problem with this string is that <math>\mathrm U</math> can occur only when paired with an <math>\mathrm A</math> or an <math>\mathrm E</math>. <!-- TODO: explain it is evaluated over multiple paths /// here is a copy-paste from the LTL page: build up from proposition variables p1,p2,..., LTL formulas are generally evaluated over paths and a position on that path. A LTL formula as such is satisfied if and only if it is satisfied for position 0 on that path. -->

CTL uses [[First-order logic#Vocabulary|atomic propositions]] as its building blocks to make statements about the states of a system. <!-- TODO: give an example of an atomic proposition. --> These propositions are then combined into formulas using [[logical operator]]s and [[temporal logic|temporal operator]]s.

Line 96:

This is denoted <math>\phi \equiv \psi</math>

It can be seen that <math>\mathrm A</math> and <math>\mathrm E</math> are duals, being universal and existential computation path quantifiers respectively:

<math>\neg \mathrm A\Phi \equiv \mathrm E \neg \Phi </math>.

Furthermore, so are <math>\mathrm G</math> and <math>\mathrm F</math>.

Hence an instance of [[De Morgan's laws]] can be formulated in CTL:

Line 108:

It can be shown using such identities that a subset of the CTL temporal connectives is adequate if it contains <math>EU</math>, at least one of <math>\{AX,EX\}</math> and at least one of <math>\{EG,AF,AU\}</math> and the boolean connectives.

The important equivalences below are called the '''expansion laws'''; they allow to unfoldunfolding the verification of a CTL connective towards its successors in time.

:<math>AG\phi \equiv \phi \land AX AG \phi</math>

:<math>EG\phi \equiv \phi \land EX EG \phi</math>

Line 145:

== Extensions ==

CTL has been extended with [[second-order logic|second-order]] quantification <math>\exists p</math> and <math>\forall p</math> to ''quantified computational tree logic'' (QCTL).<ref>{{Cite journal|last=David|first=Amélie|last2=Laroussinie|first2=Francois|last3=Markey|first3=Nicolas|date=2016|editor-last=Desharnais|editor-first=Josée|editor2-last=Jagadeesan|editor2-first=Radha|title=On the Expressiveness of QCTL|url=http://drops.dagstuhl.de/opus/volltexte/2016/6164|journal=27th [[International Conference on Concurrency Theory]] (CONCUR 2016)|series=Leibniz International Proceedings in Informatics (LIPIcs)|___location=Dagstuhl, Germany|publisher=Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik|volume=59|pages=28:1–28:15|doi=10.4230/LIPIcs.CONCUR.2016.28|isbn=978-3-95977-017-0}}</ref> There are two semantics:

* the tree semantics. We label nodes of the computation tree. QCTL* = QCTL = [[monadic second-order logic|MSO]] over trees. Model checking and satisfiability are tower complete.

Line 161:

* {{cite journal |author1=E.M. Clarke |author2=E.A. Emerson | title=Design and synthesis of synchronisation skeletons using branching time temporal logic| journal=Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science |volume=131 | publisher= Springer, Berlin | year=1981 |pages= 52–71|url=https://www.cs.cmu.edu/afs/cs/user/emc/www/papers/Invited%20Conference%20Articles/Design%20and%20Synthesis%20of%20Synchronization%20Skeletons%20Using%20Branching%20Time%20Temporal%20Logic.pdf}}

* {{cite book |author1=Michael Huth |author2=Mark Ryan | title=Logic in Computer Science (Second Edition) | year=2004| page=207 | publisher=Cambridge University Press | isbn=978-0-521-54310-1}}

* {{cite journal |author1=Emerson, E. A. |author2=Halpern, J. Y. |author2link = Joseph Halpern| title=Decision procedures and expressiveness in the temporal logic of branching time | journal=[[Journal of Computer and System Sciences]]| year=1985| volume=30 | issue=1 | pages=1–24 | doi=10.1016/0022-0000(85)90001-7}}

* {{cite journal |author1=Clarke, E. M. |author2=Emerson, E. A. |author3=Sistla, A. P. |name-list-style=amp | title=Automatic verification of finite-state concurrent systems using temporal logic specifications | journal=[[ACM Transactions on Programming Languages and Systems]]| year=1986| volume=8 | issue=2 | pages=244–263 | doi=10.1145/5397.5399}}

* {{cite book | author=Emerson, E. A. | year=1990 | chapter =Temporal and modal logic | editor=Jan van Leeuwen | editor-link=Jan van Leeuwen | title=Handbook of Theoretical Computer Science, vol. B | pages=955–1072 | publisher=MIT Press | isbn=978-0-262-22039-2}}