Verifying temporal properties of finite-state probabilistic programs
- 1 January 1988
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 338-345
- https://doi.org/10.1109/sfcs.1988.21950
Abstract
The complexity of testing whether a finite-state (sequential or concurrent) probabilistic program satisfies its specification expressed in linear temporal logic. For sequential programs an exponential-time algorithm is given and it is shown that the problem is in PSPACE; this improves the previous upper bound by two exponentials and matches the known lower bound. For concurrent programs is is shown that the problem is complete in double exponential time, improving the previous upper and lower bounds by one exponential each. These questions are also addressed for specifications described by omega -automata or formulas in extended temporal logic.Keywords
This publication has 17 references indexed in Scilit:
- The complementation problem for Büchi automata with applications to temporal logicTheoretical Computer Science, 1987
- The complexity of propositional linear temporal logicsJournal of the ACM, 1985
- Termination of Probabilistic Concurrent ProgramACM Transactions on Programming Languages and Systems, 1983
- Temporal logic can be more expressiveInformation and Control, 1983
- Reasoning with time and chanceInformation and Control, 1982
- The temporal semantics of concurrent programsTheoretical Computer Science, 1981
- AlternationJournal of the ACM, 1981
- Theories of automata on ω-tapes: A simplified approachJournal of Computer and System Sciences, 1974
- The monadic second order theory of ω1Published by Springer Nature ,1973
- Testing and generating infinite sequences by a finite automatonInformation and Control, 1966