Logics

Propositional Logics

Propositional Logics or PL is an extension of Boolean logics that handles propositional symbols. Beside the standard logical operators logical operators \(\neg\), \(\land\), \(\lor\), and \(\rightarrow\), it is also equipped with propositional variables whose Boolean values can be declared at evalutation time. An atomic proposition or AP is either a Boolean value –i.e., \(\top\) (true) or \(\bot\) (false)– or a prositional variable.

Syntax

A PL formula is either:

  • \(\top\) or \(\bot\)
  • a propositional variable
  • \(\neg\varphi_1\), \(\varphi_1 \land \varphi_2\), \(\varphi_1 \lor \varphi_2\), or \(\varphi_1 \rightarrow \varphi_2\) where both \(\varphi_1\) and \(\varphi_2\) are PL formulas

Semantics

Since pyModelChecking is primary meant to support model checking, we provide the semantics of propositional formulas with respect to a Kripke structure. If \(K\) is a Kripke structure, \(s\) one of its states, and \(\varphi\) a propositional formula, we write \(K,s \models \varphi\) (to be read “\(K\) and \(s\) satisfy \(\varphi\)”) meaning that \(\varphi\) holds at state \(s\) in \(K\).

Let \(K\) be the Kripke structure \((S,S_0,R,L)\); the relation \(\models\) is defined recursively as follows:

  • \(K,s \models \top\) and \(K,s \not\models \bot\) for any state \(s \in S\)
  • if \(p \in AP\), then \(K,s \models p\) \(\Longleftrightarrow\) \(p \in L(s)\)
  • \(K,s \models \neg\varphi\) \(\Longleftrightarrow\) \(K,s \not\models \varphi\)
  • \(K,s \models \varphi_1 \land \varphi_2\) \(\Longleftrightarrow\) \(K,s \models \varphi_1\) and \(K,s \models \varphi_2\)
  • \(K,s \models \varphi_1 \lor \varphi_2\) \(\Longleftrightarrow\) \(K,s \models \varphi_1\) or \(K,s \models \varphi_2\)
  • \(K,s \models \varphi_1 \rightarrow \varphi_2\) \(\Longleftrightarrow\) \(K,s \not\models \varphi_1\) or \(K,s \models \varphi_2\)

Computational Tree Logic*

The Computational Tree Language* or CTL* is a the temporal logic that describes the properties of computation trees over Kripke structures ([CE81], [CES86]). It is a proper extension of propositional logics and, beside a set of atomic propostions and the standard logical operators \(\neg\), \(\land\), \(\lor\), and \(\rightarrow\), the alphabet of CTL* contains the two path quantifiers \(\mathbf{A}\) (“for all paths”) and \(\mathbf{E}\) (“for some path”) and the five temporal operators \(\mathbf{X}\) (“at the next step”), \(\mathbf{G}\) (“globally”), \(F\) (“in the future”), \(\mathbf{U}\) (“until”), and \(\mathbf{R}\) (“release”).

Syntax

Any CTL* formula is either a state formula (i.e., a formula that are evaluated in a single state) or a path formula (i.e., a formula whose truth value depend on an infinite path).

A CTL* state formula is either:

  • \(\top\) or \(\bot\)
  • a propositional variable
  • \(\neg\varphi_1\), \(\varphi_1 \land \varphi_2\), \(\varphi_1 \lor \varphi_2\), or \(\varphi_1 \rightarrow \varphi_2\) where both \(\varphi_1\) and \(\varphi_2\) are CTL* state formulas
  • \(\mathbf{A} \psi\) or \(\mathbf{E} \psi\) where \(\psi\) is a CTL* path formula

A CTL* path formula is either:

  • a state formula
  • \(\neg\psi_1\), \(\psi_1 \land \psi_2\), \(\psi_1 \lor \psi_2\), or \(\psi_1 \rightarrow \psi_2\) where both \(\psi_1\) and \(\psi_2\) are CTL* path formulas
  • \(\mathbf{X} \psi_1\), \(\mathbf{F} \psi_1\), \(\mathbf{G} \psi_1\), \(\psi_1 \mathbf{U} \psi_2\), or \(\psi_1 \mathbf{R} \psi_2\) where both \(\psi_1\) and \(\psi_2\) are CTL* path formulas

Semantics

The semantics of CTL* formulas is given with respect to a Kripke structure and it is a proper extension of the sematics of propositional logics. If \(K\) is a Kripke structure, \(s\) one of its states, and \(\varphi\) a state formula, we write \(K,s \models \varphi\) meaning that \(\varphi\) holds at state \(s\) in \(K\). Analogously, If \(K\) is a Kripke structure, \(\pi\) one of its computations, and \(\psi\) a path formula, we write \(K,\pi \models \psi\) meaning that \(\psi\) holds along \(\pi\) in \(K\).

Let \(K\) be the Kripke structure \((S,S_0,R,L)\); the relation \(\models\) is defined recursively as follows:

  • \(K,s \models \top\) and \(K,s \not\models \bot\) for any state \(s \in S\)
  • if \(p \in AP\), then \(K,s \models p\) \(\Longleftrightarrow\) \(p \in L(s)\)
  • \(K,s \models \neg\varphi\) \(\Longleftrightarrow\) \(K,s \not\models \varphi\)
  • \(K,s \models \varphi_1 \land \varphi_2\) \(\Longleftrightarrow\) \(K,s \models \varphi_1\) and \(K,s \models \varphi_2\)
  • \(K,s \models \varphi_1 \lor \varphi_2\) \(\Longleftrightarrow\) \(K,s \models \varphi_1\) or \(K,s \models \varphi_2\)
  • \(K,s \models \varphi_1 \rightarrow \varphi_2\) \(\Longleftrightarrow\) \(K,s \not\models \varphi_1\) or \(K,s \models \varphi_2\)
  • \(K,s \models \mathbf{A} \varphi\) \(\Longleftrightarrow\) \(K,\pi \models \varphi\) for any computation \(\pi\) of \(K\) that starts from \(s\)
  • \(K,s \models \mathbf{E} \varphi\) \(\Longleftrightarrow\) \(K,\pi \models \varphi\) for some computation \(\pi\) of \(K\) that starts from \(s\)
  • \(K,\pi \models \psi\) \(\Longleftrightarrow\) \(K,s \models \psi\), where \(\pi\) is a computation of \(K\) that starts from \(s\)
  • \(K,\pi \models \neg\psi\) \(\Longleftrightarrow\) \(K,\pi \not\models \psi\)
  • \(K,\pi \models \psi_1 \land \psi_2\) \(\Longleftrightarrow\) \(K,\pi \models \psi_1\) and \(K,\pi \models \psi_2\)
  • \(K,\pi \models \psi_1 \lor \psi_2\) \(\Longleftrightarrow\) \(K,\pi \models \psi_1\) or \(K,\pi \models \psi_2\)
  • \(K,\pi \models \psi_1 \rightarrow \psi_2\) \(\Longleftrightarrow\) \(K,\pi \not\models \psi_1\) or \(K,\pi \models \psi_2\)
  • \(K,\pi \models \mathbf{X} \psi\) \(\Longleftrightarrow\) \(K,\pi_1 \models \psi\)
  • \(K,\pi \models \mathbf{F} \psi\) \(\Longleftrightarrow\) \(K,\pi_i \models \psi\) for some \(i \in \mathbb{N}\)
  • \(K,\pi \models \mathbf{G} \psi\) \(\Longleftrightarrow\) \(K,\pi_i \models \psi\) for all \(i \in \mathbb{N}\)
  • \(K,\pi \models \psi_1 \mathbf{U} \psi_2\) \(\Longleftrightarrow\) there exists an \(i \in \mathbb{N}\) such that \(K,\pi_i \models \psi_2\) and \(K,\pi_j \models \psi_1\) for all \(j \in [0,i-1]\)
  • \(K,\pi \models \psi_1 \mathbf{R} \psi_2\) \(\Longleftrightarrow\) for all \(i \in \mathbb{N}\), if \(K,\pi_j \not\models \psi_1\) for all \(j \in [0,i-1]\), then \(K,\pi_i \models \psi_2\)

Whenever \(K,\sigma \models \psi\) \(\Longleftrightarrow\) \(K,\sigma \models \varphi\) for any \(\sigma\) and and any \(K\), we say that \(\psi\) and \(\varphi\) are equivalent and we write \(\varphi \equiv \psi\).

Two set of formulas \(\mathcal{F}\) and and any \(\mathbf{G}\) are equivalent if any formula \(\mathbf{G}\) has an equivalent formula in \(\mathcal{F}\) and vice versa.

Restricted Syntax

It is easy to prove that \(\bot\), \(\mathbf{F} \psi\), \(\mathbf{G} \psi\), \(\varphi \mathbf{R} \psi\), \(\mathbf{A} \varphi\), \(\varphi \land \psi\), and \(\varphi \rightarrow \psi\) are equivalent to \(\neg \top\), \(\top \mathbf{U} \psi\), \(\neg (\top \mathbf{U} \neg \psi)\), \(\neg (\neg \varphi \mathbf{U} \neg \psi)\), \(\neg \mathbf{E} \neg \varphi\), \(\neg (\varphi \lor \psi)\), and \(\neg \varphi \lor \psi\), respectively. Thus, the CTL* language whose alphabet is restricted to \(\neg\), \(\lor\), \(\mathbf{X}\), \(\mathbf{U}\), \(\mathbf{A}\), \(\top\), and atomic propositions is equivalent to the full CTL* language (e.g., see [CGP00]).

Computational Tree Logic

The Computational Tree Language or CTL is a subset of CTL* ([BMP83], [CE81], [CE80]). In CTL, each occurence of the two path quantifiers \(\mathbf{A}\) and \(\mathbf{E}\) should be coupled to one of the temporal operators \(\mathbf{X}\), \(\mathbf{G}\), \(\mathbf{F}\), \(\mathbf{U}\), or \(\mathbf{U}\).

Syntax

More formally, a CTL state formula is either:

  • \(\top\) or \(\bot\)
  • propositional variable
  • \(\neg \varphi_1\), \(\varphi_1 \land \varphi_2\), \(\varphi_1 \lor \varphi_2\), or \(\varphi_1 \rightarrow \varphi_2\), where both \(\varphi_1\) and \(\varphi_2\) are CTL state formulas
  • \(\mathbf{A} \psi\) or \(\mathbf{E} \psi\) where \(\varphi\) is a CTL path formula

A CTL path formula is either \(\mathbf{X} \varphi_1\), \(\mathbf{F} \varphi_1\), \(\mathbf{G} \varphi_1\), \(\varphi_1 \mathbf{U} \varphi_2\), or \(\varphi_1 \mathbf{R} \varphi_2\) where both \(\varphi_1\) and \(\varphi_2\) are CTL state formulas.

Semantics

CTL has the same semantics of CTL*.

Restricted Syntax

Despite the apperent syntatic complexity of CTL, any possible property definable in it can be expressed by a CTL formula whose syntax is restricted to the use of \(\top\), \(\neg\), \(\lor\), and \(\mathbf{E}\) coupled to either \(\mathbf{X}\), \(\mathbf{U}\), or \(\mathbf{G}\) (e.g., see [CGP00]). As a matter of the facts, it is easy to prove that:

  • \(\bot \equiv \neg \top\)
  • \(\varphi_1 \land \varphi_2 \equiv \neg (\neg \varphi_1 \lor \neg \varphi_2)\)
  • \(\varphi_1 \rightarrow \varphi_2 \equiv \neg \varphi_1 \lor \varphi_2\)
  • \(\mathbf{A}\mathbf{X} \varphi \equiv \neg \mathbf{E}\mathbf{X} (\neg \varphi)\)
  • \(\mathbf{E}F \varphi \equiv \mathbf{E}(\top \mathbf{U} \varphi)\)
  • \(\mathbf{A}\mathbf{G} \varphi \equiv \neg \mathbf{E}(\top \mathbf{U} \neg \varphi)\)
  • \(\mathbf{A}F \varphi \equiv \neg \mathbf{E}\mathbf{G} (\neg \varphi)\)
  • \(\mathbf{A}(\varphi_1 \mathbf{U} \varphi_2) \equiv \neg (\mathbf{E} ((\neg \varphi_2) \mathbf{U} \neg (\varphi_1 \lor \varphi_2) ) \lor \mathbf{E}\mathbf{G}(\neg \varphi_2))\)
  • \(\mathbf{A}(\varphi_1 \mathbf{R} \varphi_2) \equiv \neg \mathbf{E} ((\neg \varphi_1) \mathbf{U} (\neg \varphi_2))\)
  • \(\mathbf{E}(\varphi_1 \mathbf{R} \varphi_2) \equiv (\mathbf{E} (\varphi_2 \mathbf{U} (\neg \varphi_1 \lor \neg \varphi_2) ) \lor \mathbf{E}\mathbf{G}(\varphi_2))\)

Linear Time Logic

The Linear Time Logic or LTL is a subset of of CTL* ([P77]).

Syntax

LTL formulas have the form \(A \rho\) where \(\rho\) is a LTL path formula and a LTL path formula is either:

  • \(\top\) or \(\bot\)
  • propositional variable
  • \(\neg \varphi_1\), \(\varphi_1 \land \varphi_2\), \(\varphi_1 \lor \varphi_2\), or \(\varphi_1 \rightarrow \varphi_2\), where both \(\varphi_1\) and \(\varphi_2\) are LTL path formulas
  • \(\mathbf{X} \varphi_1\), \(\mathbf{F} \varphi_1\), \(\mathbf{G} \varphi_1\), \(\varphi_1 \mathbf{U} \varphi_2\), or \(\varphi_1 \mathbf{R} \varphi_2\) where both \(\varphi_1\) and \(\varphi_2\) are LTL path formulas.

Semantics

LTL has the same semantics of CTL*.

Restricted Syntax

It is easy to prove that:

  • \(\psi_1 \land \psi_2 \equiv \neg (\neg \psi_1 \lor \neg \psi_2)\)
  • \(\psi_1 \rightarrow \psi_2 \equiv \neg \psi_1 \lor \psi_2\)
  • \(\mathbf{F} \psi \equiv \top \mathbf{U} \psi\)
  • \(\mathbf{G} \psi \equiv \neg (\top \mathbf{U} \neg \psi)\)
  • \(\psi_1 \mathbf{R} \psi_2 \equiv \neg ((\neg \psi_1) \mathbf{U} (\neg \psi_2))\)

Hence, the LTL restricted language that allows exclusively the path formulas whose operators are \(\neg\), \(\lor\), \(\mathbf{X}\), or \(\mathbf{U}\) is equivalent to the full LTL language (e.g., see [CGP00]).

[P77]A. Pnueli. “The temporal logic of programs.” In Proceedings of the 18th Annual Symposium of Foundations of Computer Science (FOCS), 1977, 46-57
[BMP83]M. Ben-Ari, Z. Manna, A. Pnueli. The temporal logic of branching time. Acta Informatica 20(1983): 207-226
[CE81](1, 2) E. M. Clarke, E. A. Emerson. “Design and synthesis of synchronization skeletons using branching time temporal logic.” In Logic of Programs: Workshop. LNCS 131. Springer, 1981.
[CE80]E. M. Clarke, E. A. Emerson. “Characterizing correcteness properties of parallel programs using fixpoints.” In Automata, Languages, and Programming. LNCS 85:169-181. Springer 1980.
[CES86]E. M. Clarke, E. A. Emerson, A. P. Sistla. “Automatic verification of finite-state concurrent systems using temporal logic specifications.” ACM Transactions on Programming Languages and Systems 8(2): 244-263. 1986.
[CGP00](1, 2, 3) E. M. Clarke, O. Grumberg, D. A. Peled. “Model Checking” MIT Press, Cambridge, MA, USA. 2000.