# 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
Full Text:
##### References:
  Barwise, J., Admissible sets and structures, (1975), Springer · Zbl 0316.02047  Ben-Ari, M.; Pnueli, A.; Manna, Z., The temporal logic of branching time, Acta Inform., 20, 3, 207-226, (1983) · Zbl 0533.68036  Burgess, J., Logic and time, J. Symb. Log., 44, 4, 566-582, (1979) · Zbl 0423.03018  Burgess, J., Decidability for branching time, Stud. Log., 39, 2-3, 213-218, (1980) · Zbl 0467.03006  Burgess, J., Axioms for tense logic. I. “since“ and “until”, Notre Dame J. Form. Log., 23, 4, 367-374, (1982) · Zbl 0452.03021  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  Demri, S.; Nowak, D., Reasoning about transfinite sequences, Int. J. Found. Comput. Sci., 18, 1, 87-112, (2007) · Zbl 1109.68065  Demri, S.; Rabinovich, A., The complexity of temporal logic with until and Since over ordinals, Log. Methods Comput. Sci., 6, 4, (2010)  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)  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  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  Emerson, E.; Clarke, E., Using branching time logic to synthesize synchronization skeletons, Sci. Comput. Program., 2, 241-266, (1982) · Zbl 0514.68032  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  Feldman, Y., A decidable propositional dynamic logic with explicit probabilities, Inf. Control, 63, 11-38, (1984) · Zbl 0592.68031  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  Gabbay, D.; Hodkinson, I.; Reynolds, M., Temporal logic, Mathematical Foundations and Computational Aspects, vol. 1, (1994), Clarendon Press Oxford · Zbl 0921.03023  Gargantini, A.; Mandrioli, D.; Morzenti, A., Dealing with zero-time transitions in axiom systems, Inf. Comput., 150, 2, 119-131, (1999) · Zbl 1045.68591  Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. Asp. Comput., 6, 5, 512-535, (1994) · Zbl 0820.68113  Lehmann, D.; Shelah, S., Reasoning with time and chance, Inf. Control, 53, 165-198, (1982) · Zbl 0523.03016  Ognjanović, Zoran, Discrete linear-time probabilistic logics: completeness, decidability and complexity, J. Log. Comput., 16, 2, 257-285, (2006) · Zbl 1102.03022  Pnueli, A., The temporal logic of programs, (Proceedings of the 18th IEEE Symposium Foundations of Computer Science (FOCS 1977), (1977)), 46-57  Prior, A., Time and modality, (1957), Oxford University Press · Zbl 0079.00606  Reynolds, M., An axiomatization of full computation tree logic, J. Symb. Log., 66, 3, 1011-1057, (2001) · Zbl 1002.03015  Sistla, A.; Clarke, E., The complexity of propositional linear temporal logic, J. ACM, 32, 3, 733-749, (1985) · Zbl 0632.68034  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.