×

zbMATH — the first resource for mathematics

A propositional linear time logic with time flow isomorphic to \(\omega^2\). (English) Zbl 1328.03017
Summary: Primarily guided with the idea to express zero-time transitions by means of temporal propositional language, we have developed a temporal logic where the time flow is isomorphic to ordinal \(\omega^2\) (concatenation of \(\omega\) copies of \(\omega\)). If we think of \(\omega^2\) as lexicographically ordered \(\omega\times\omega\), then any particular zero-time transition can be represented by states whose indices are all elements of some \(\{n\}\times\omega\). In order to express non-infinitesimal transitions, we have introduced a new unary temporal operator \([\omega]\) (\(\omega\)-jump), whose effect on the time flow is the same as the effect of \(\alpha\mapsto\alpha+\omega\) in \(\omega^2\). In terms of lexicographically ordered \(\omega\times\omega\), \([\omega]\phi\) is satisfied in \(\langle i,j\rangle\)-th time instant iff \(\phi\) is satisfied in \(\langle i+1,0\rangle\)-th time instant. Moreover, in order to formally capture the natural semantics of the until operator U, we have introduced a local variant u of the until operator. More precisely, \(\phi\) u \(\psi\) is satisfied in \(\langle i,j\rangle\)-th time instant iff \(\psi\) is satisfied in \(\langle i,j+k\rangle\)-th time instant for some nonnegative integer \(k\), and \(\phi\) is satisfied in \(\langle i,j+l\rangle\)-th time instant for all \(0\leq l<k\). As in many of our previous publications, the leitmotif is the usage of infinitary inference rules in order to achieve the strong completeness.

MSC:
03B44 Temporal logic
03B25 Decidability of theories and sets of sentences
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Barwise, J., Admissible sets and structures, (1975), Springer · Zbl 0316.02047
[2] Ben-Ari, M.; Pnueli, A.; Manna, Z., The temporal logic of branching time, Acta Inform., 20, 3, 207-226, (1983) · Zbl 0533.68036
[3] Burgess, J., Logic and time, J. Symb. Log., 44, 4, 566-582, (1979) · Zbl 0423.03018
[4] Burgess, J., Decidability for branching time, Stud. Log., 39, 2-3, 213-218, (1980) · Zbl 0467.03006
[5] Burgess, J., Axioms for tense logic. I. “since“ and “until”, Notre Dame J. Form. Log., 23, 4, 367-374, (1982) · Zbl 0452.03021
[6] Burgess, J., Basic tense logic, (Gabbay, D.; Guenthner, F., Handbook of Philosophical Logic, vol. II, (1984), D. Reidel Publishing Company), 89-133 · Zbl 0875.03046
[7] Demri, S.; Nowak, D., Reasoning about transfinite sequences, Int. J. Found. Comput. Sci., 18, 1, 87-112, (2007) · Zbl 1109.68065
[8] Demri, S.; Rabinovich, A., The complexity of temporal logic with until and Since over ordinals, Log. Methods Comput. Sci., 6, 4, (2010)
[9] Doder, D.; Marković, Z.; Ognjanović, Z.; Perović, A.; Rašković, M., A probabilistic temporal logic that can model reasoning about evidence, Lect. Notes Comput. Sci., 5956, 9-24, (2010)
[10] Doder, D.; Ognjanović, Z.; Marković, Z., An axiomatization of a first-order branching time temporal logic, J. Univers. Comput. Sci., 16, 11, 1439-1451, (2010) · Zbl 1216.03033
[11] Emerson, E., Temporal and modal logic, (van Leeuwen, J., Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, (1990), North-Holland Pub. Co./MIT Press), 995-1072 · Zbl 0900.03030
[12] Emerson, E.; Clarke, E., Using branching time logic to synthesize synchronization skeletons, Sci. Comput. Program., 2, 241-266, (1982) · Zbl 0514.68032
[13] Emerson, E.; Halpern, J., Decision procedures and expressiveness in the temporal logic of branching time, J. Comput. Syst. Sci., 30, 1, 1-24, (1985) · Zbl 0559.68051
[14] Feldman, Y., A decidable propositional dynamic logic with explicit probabilities, Inf. Control, 63, 11-38, (1984) · Zbl 0592.68031
[15] Ferrucci, L.; Mandrioli, D.; Morzenti, A.; Rossi, M., A metric temporal logic for dealing with zero-time transitions, (International Symposium on Temporal Representation and Reasoning, (2012)), 81-88
[16] Gabbay, D.; Hodkinson, I.; Reynolds, M., Temporal logic, Mathematical Foundations and Computational Aspects, vol. 1, (1994), Clarendon Press Oxford · Zbl 0921.03023
[17] Gargantini, A.; Mandrioli, D.; Morzenti, A., Dealing with zero-time transitions in axiom systems, Inf. Comput., 150, 2, 119-131, (1999) · Zbl 1045.68591
[18] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. Asp. Comput., 6, 5, 512-535, (1994) · Zbl 0820.68113
[19] Lehmann, D.; Shelah, S., Reasoning with time and chance, Inf. Control, 53, 165-198, (1982) · Zbl 0523.03016
[20] Ognjanović, Zoran, Discrete linear-time probabilistic logics: completeness, decidability and complexity, J. Log. Comput., 16, 2, 257-285, (2006) · Zbl 1102.03022
[21] Pnueli, A., The temporal logic of programs, (Proceedings of the 18th IEEE Symposium Foundations of Computer Science (FOCS 1977), (1977)), 46-57
[22] Prior, A., Time and modality, (1957), Oxford University Press · Zbl 0079.00606
[23] Reynolds, M., An axiomatization of full computation tree logic, J. Symb. Log., 66, 3, 1011-1057, (2001) · Zbl 1002.03015
[24] Sistla, A.; Clarke, E., The complexity of propositional linear temporal logic, J. ACM, 32, 3, 733-749, (1985) · Zbl 0632.68034
[25] Stirling, C., Modal and temporal logic, (Handbook of Logic in Computer Science, vol. 2, (1992)), 477-563
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.