Content deleted Content added
No edit summary |
Tom.Reding (talk | contribs) m Enum 1 author/editor WL; WP:GenFixes on |
||
Line 28:
:<math>\mbox{EF }\big(r \mbox{ U } q\big) </math>
The problem with this string is that <math>U</math> can occur only when paired with an <math>A</math> or an <math>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 164:
* {{cite journal |author1=Emerson, E. A. |author2=Halpern, J. Y. | 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=
==External links==
| |||