
A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.
linear time temporal logic, Logic in computer science, Specification and verification (program logics, model checking, etc.), exponential time decision procedure, Logic, Temporal logic, Expressive completeness, Axiomatizations, Automata and formal grammars in connection with logical questions, propositional dynamic logic, Dynamic logic, ω-automata, Linear time temporal logic, expressive completeness, \(\omega\)-automata, finitary axiomatization, DLTL, monadic second-order theory of \(\omega\)-sequences
linear time temporal logic, Logic in computer science, Specification and verification (program logics, model checking, etc.), exponential time decision procedure, Logic, Temporal logic, Expressive completeness, Axiomatizations, Automata and formal grammars in connection with logical questions, propositional dynamic logic, Dynamic logic, ω-automata, Linear time temporal logic, expressive completeness, \(\omega\)-automata, finitary axiomatization, DLTL, monadic second-order theory of \(\omega\)-sequences
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 73 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
