A decidable and expressive fragment of Many-Sorted First-Order Linear Temporal Logic.

Quentin Peyras Julien Brunel David Chemouil

Published in: Inf. Comput. (2021)

Keyphrases

finite state
linear temporal logic
model checking
temporal logic
automata theoretic
linear time temporal logic
bounded model checking
transition systems
modal logic
concurrent systems
first order logic
reactive systems
tight complexity bounds