
arXiv: 1306.2141
handle: 11383/2027988
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability---where no more than v events may occur every V time units, for given v, V. When reasoning about formulas with intrinsic bounded variability, one can employ the simpler techniques that rely on bounded variability, without any loss of generality. What is then the complexity of algorithmically deciding which formulas have intrinsic bounded variability? In this paper, we study the problem with reference to Metric Temporal Logic (MTL). We prove that deciding bounded variability of MTL formulas is undecidable over dense-time models, but with a undecidability degree lower than generic dense-time MTL satisfiability. Over discrete-time models, instead, deciding MTL bounded variability has the same exponential-space complexity as satisfiability. To complement these negative results, we also briefly discuss small fragments of MTL that are more amenable to reasoning about bounded variability.
FOS: Computer and information sciences, Logic in computer science, Computer Science - Logic in Computer Science, Applied Mathematics, decidability, Temporal logic, Automata and formal grammars in connection with logical questions, Logic in Computer Science (cs.LO), Decidability of theories and sets of sentences, metric temporal logic, Artificial Intelligence, bounded variability, Mathematics (all), Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), complexity
FOS: Computer and information sciences, Logic in computer science, Computer Science - Logic in Computer Science, Applied Mathematics, decidability, Temporal logic, Automata and formal grammars in connection with logical questions, Logic in Computer Science (cs.LO), Decidability of theories and sets of sentences, metric temporal logic, Artificial Intelligence, bounded variability, Mathematics (all), Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), complexity
| selected citations These citations are derived from selected sources. 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). | 2 | |
| 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. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
