"Most of" leads to undecidability: Failure of adding frequencies to LTL

Bartosz BednarczykBartosz Bednarczyk, Jakub MichaliszynJakub Michaliszyn

Bartosz Bednarczyk, Jakub Michaliszyn
"Most of" leads to undecidability: Failure of adding frequencies to LTL
In Stefan Kiefer, Christine Tasson, eds., Proceedings of the Foundations of Software Science and Computation Structures - 24th International Conference (FOSSACS 2021), volume 12650 of Lecture Notes in Computer Science, 82--101, March 2021. Springer

Details
Bibtex

KurzfassungAbstract
Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and briefly discuss how the undecidability results transfer to first-order logic on words.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-71995-1\_5.

@inproceedings{BM2021,
  author    = {Bartosz Bednarczyk and Jakub Michaliszyn},
  title     = {"Most of" leads to undecidability: Failure of adding frequencies
               to {LTL}},
  editor    = {Stefan Kiefer and Christine Tasson},
  booktitle = {Proceedings of the Foundations of Software Science and
               Computation Structures - 24th International Conference (FOSSACS
               2021)},
  series    = {Lecture Notes in Computer Science},
  volume    = {12650},
  publisher = {Springer},
  year      = {2021},
  month     = {March},
  pages     = {82--101},
  doi       = {10.1007/978-3-030-71995-1\_5}
}