Decision Procedures for Time and Chance (Extended 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.

Authors

• Sarit Kraus
• Daniel Lehmann 0001

Keywords

• Page description languages
• Mathematics
• Computer science
• Probabilistic logic
• Power system modeling
• Decision Problem
• Log Time
• Exponential Time
• Generation Sequencing
• Linear Time
• Sequence Of States
• Universal Model
• Equivalence Relation
• Binary Relation
• Induction Hypothesis
• Mutatis Mutandis
• Temporal Logic
• Set Of Formulas