Decision procedures for time and chance
- 1 November 1983
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 202-209
- https://doi.org/10.1109/sfcs.1983.12
Abstract
Decision procedures are provided for checking the satisfiability of a formula in each of the three systems TCg. TCb and TCf defined in [LS]. The procedures for TCg and TCf run in non-deterministic time 22on where n is the size of the formula and c is a constant. The procedure for TCb runs in non-deterministic time 22on2. A deterministic exponential lower bound is proved for the three systems. All three systems are also shown to be PSPACE-hard using results of [SC]. Those decision procedures are not as efficient as the deterministic (one or two)- exponential time procedures proposed in [BMP] and [EH1] for different logics of branching time that are weaker than ours in expressive power. No elementary decision procedure is known for a logic of branching time that is as expressive as ours. The decision procedures of the probabilistic logics of [HS] run in deterministic exponential time but their language is essentially less expressive than ours.Keywords
This publication has 14 references indexed in Scilit:
- “Sometimes” and “not never” revisitedJournal of the ACM, 1986
- Reasoning with time and chancePublished by Springer Nature ,1983
- Symmetric and economical solutions to the mutual exclusion problem in a distributed systemPublished by Springer Nature ,1983
- N-Process mutual exclusion with bounded waiting by 4 · Log2 N-valued shared variableJournal of Computer and System Sciences, 1982
- The choice coordination problemActa Informatica, 1982
- The complexity of propositional linear temporal logicsPublished by Association for Computing Machinery (ACM) ,1982
- The temporal semantics of concurrent programsTheoretical Computer Science, 1981
- On the andvantages of free choicePublished by Association for Computing Machinery (ACM) ,1981
- "Sometime" is sometimes "not never"Published by Association for Computing Machinery (ACM) ,1980
- Decidability of Second-Order Theories and Automata on Infinite TreesTransactions of the American Mathematical Society, 1969