Alternating automata and temporal logic normal forms. (English) Zbl 1087.03013
Summary: We provide a translation from \(\text{SNF}_{\text{PLTL}}\), a normal form for propositional linear time temporal logic, into alternating automata on infinite words, and vice versa. We show this translation has the property that the set of \(\text{SNF}_{\text{PLTL}}\) clauses is satisfiable if and only if the alternating automaton has an accepting run. As there is no direct method known for checking the non-emptiness of alternating automata, the translation to \(\text{SNF}_{\text{PLTL}}\), together with a temporal proof on the resulting \(\text{SNF}_{\text{PLTL}}\) clauses, provides an indirect non-emptiness check for alternating automata.
MSC:
| 03B44 | Temporal logic |
| 68Q45 | Formal languages and automata |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | The Imperative Future: Principles of Executable Temporal Logic, (Barringer, H.; Fisher, M.; Gabbay, D.; Owens, R.; Reynolds, M. (1996), Research Studies Press) |
| [2] | Bolotov, A., Clausal resolution for extended computation tree logic ECTL, (Reynolds, M.; Sattar, A., Proceedings of the Tenth International Symposium on Temporal Representation and Reasoning and the Fourth International Conference on Temporal Logic. Proceedings of the Tenth International Symposium on Temporal Representation and Reasoning and the Fourth International Conference on Temporal Logic, TIME-ICTL 2003, July 2003, Cairns, Australia (2003), IEEE Computer Society Press), 110-117 · Zbl 1101.03017 |
| [3] | Bolotov, A.; Basukoski, A., A clausal resolution method for CTL branching-time logic \(ECTL^+\), (Proceedings of TIME 2004 the Eleventh International Symposium on Temporal Representation and Reasoning. Proceedings of TIME 2004 the Eleventh International Symposium on Temporal Representation and Reasoning, July 2004, Tatihou, Normandie, France (2004), IEEE Computer Society Press) · Zbl 1101.03017 |
| [4] | Bolotov, A.; Fisher, M., A clausal resolution method for CTL branching time temporal logic, Journal of Experimental and Theoretical Artificial Intelligence, 11, 77-93 (1999) · Zbl 1054.68666 |
| [5] | Bolotov, A.; Fisher, M.; Dixon, C., On the relationship between \(\omega \)-automata and temporal logic normal forms, Journal of Logic and Computation, 12, 4, 261-581 (2002) · Zbl 1007.03014 |
| [6] | Brzozowski, J.; Leiss, E., Finite automata, and sequential networks, Theoretical Computer Science, 10, 19-35 (1980) · Zbl 0415.68023 |
| [7] | Chandra, A.; Kozen, D.; Stockmeyer, L., Alternation, ACM Journal, 28, 1, 114-133 (1981) · Zbl 0473.68043 |
| [8] | Dasgupta, P.; Chakrabarti, P. P.; DeSarkar, S. C., Multi-objective heuristic search in AND/OR graphs, Journal of Algorithms, 20, 2, 282-311 (1996) · Zbl 0852.68016 |
| [9] | Dixon, C.; Fisher, M.; Wooldridge, M., Resolution for temporal logics of knowledge, Journal of Logic and Computation, 8, 3, 345-372 (1998) · Zbl 0951.03007 |
| [10] | Emerson, E. A., Temporal and modal logic, (van Leeuwen, J., Handbook of Theoretical Computer Science (1990), Elsevier Science Publishers B.V.: Elsevier Science Publishers B.V. Amsterdam, The Netherlands), 996-1072 · Zbl 0900.03030 |
| [11] | E.A. Emerson, C.-L. Lei, Modalities for model checking: Branching time logic strikes back, in: Proceedings of the Twelfth ACM Symposium on the Principles of Programming Languages, January 1985, pp. 84-96; E.A. Emerson, C.-L. Lei, Modalities for model checking: Branching time logic strikes back, in: Proceedings of the Twelfth ACM Symposium on the Principles of Programming Languages, January 1985, pp. 84-96 |
| [12] | E.A. Emerson, C.-L. Lei, Temporal model checking under generalized fairness constraints, in: Proceedings of the Eighteenth Hawaii International Conference on System Sciences, 1985, pp. 277-288; E.A. Emerson, C.-L. Lei, Temporal model checking under generalized fairness constraints, in: Proceedings of the Eighteenth Hawaii International Conference on System Sciences, 1985, pp. 277-288 |
| [13] | Fisher, M., A normal form for temporal logic and its application in theorem-proving and execution, Journal of Logic and Computation, 7, 4, 429-456 (1997) · Zbl 0893.03003 |
| [14] | Fisher, M.; Dixon, C.; Peim, M., Clausal temporal resolution, ACM Transactions on Computational Logic, 2, 1, 12-56 (2001) · Zbl 1365.03017 |
| [15] | Hustadt, U.; Dixon, C.; Schmidt, R. A.; Fisher, M., Normal forms and proofs in combined modal and temporal logics, (Proceedings of the Third International Workshop on Frontiers of Combining Systems. Proceedings of the Third International Workshop on Frontiers of Combining Systems, FroCoS’2000. Proceedings of the Third International Workshop on Frontiers of Combining Systems. Proceedings of the Third International Workshop on Frontiers of Combining Systems, FroCoS’2000, LNAI, vol. 1794 (2000), Springer), Extended version of the paper with the same name and authors published · Zbl 0964.03011 |
| [16] | Miyano, S.; Hayashi, T., Alternating finite automata on \(\omega \)-words, Theoretical Computer Science, 32, 321-330 (1984) · Zbl 0544.68042 |
| [17] | Nilsson, N. J., Problem-Solving Methods in Artificial Intelligence (1971), McGraw-Hill: McGraw-Hill New York |
| [18] | Vardi, M.; Wolper, P., Reasoning about infinite computations, Information and Computation, 115, 1, 1-37 (1994) · Zbl 0827.03009 |
| [19] | Vardi, M. Y., An automata-theoretic approach to linear temporal logic, (Proceedings of the VIII Banff Higher Order Workshop. Proceedings of the VIII Banff Higher Order Workshop, Lecture Notes in Computer Science, vol. 1043 (1996), Springer-Verlag), 238-266 · Zbl 1543.68236 |
| [20] | Vardi, M. Y., Alternating automata: Checking truth and validity for temporal logics, (Proeeedings of the 14th International Conference on Automated Deduction. Proeeedings of the 14th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1249 (1997), Springer-Verlag), 191-206 · Zbl 1430.68156 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
