Decision procedures and expressiveness in the temporal logic of branching time (Q2265816): Difference between revisions
From MaRDI portal
Created claim: Wikidata QID (P12): Q56432687, #quickstatements; #temporary_batch_1710862453543 |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/0022-0000(85)90001-7 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2067441543 / rank | |||
Normal rank | |||
Revision as of 01:37, 20 March 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Decision procedures and expressiveness in the temporal logic of branching time |
scientific article |
Statements
Decision procedures and expressiveness in the temporal logic of branching time (English)
0 references
1985
0 references
\textit{E. A. Emerson} and \textit{E. M. Clarke} [Sci. Comput. Program. 2, 241- 266 (1982; Zbl 0514.68032)] have proposed the computation tree logic (CTL), which is the unified branching time logic (UB) of \textit{M. Ben- Ari}, \textit{Z. Manna} and \textit{A. Pnueli} [8th ACM Symp. on Principles of Programming Languages, 164-176 (1981)] augmented with an until operator. This paper gives an exponential decision procedure for deciding satisfiability in CTL with the small model theorem and its complete axiomatization. The relative expressive power of temporal logics obtained by extending or restricting the syntax of UB and CTL is also studied.
0 references
completeness
0 references
computation tree logic
0 references
unified branching time logic
0 references
exponential decision procedure
0 references
satisfiability
0 references
CTL
0 references
small model theorem
0 references
complete axiomatization
0 references
relative expressive power
0 references
UB
0 references
