Fair computational tree logic: Difference between revisions

Revision as of 18:20, 6 December 2020

Latest revision as of 06:51, 15 August 2023

(4 intermediate revisions by 4 users not shown)

Line 1:

{{No footnotes|date=April 2023}}

'''Fair computational tree logic''' is conventional [[computational tree logic]] studied with explicit fairness constraints.

Line 4 ⟶ 5:

This declares conditions such as all processes execute infinitely often. If you consider the processes to be P_i, then the condition becomes:

:<math>\bigwedge EFP_GFP_{i}</math>

==Strong fairness / compassion==

Line 37 ⟶ 38:

==References==

* {{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| doi-access=free}}

* {{cite journal |author1=Clarke, E. M. |author1link = Edmund M. Clarke|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| s2cid=52853200 | doi-access=free }}

[[Category:Temporal logic]]