Weight Monitoring with Linear Temporal Logic: Complexity and Decidability

Christel BaierChristel Baier, Joachim KleinJoachim Klein, Sascha KlüppelholzSascha Klüppelholz, Sascha WunderlichSascha Wunderlich

DOI Link

Christel Baier, Joachim Klein, Sascha Klüppelholz, Sascha Wunderlich
Weight Monitoring with Linear Temporal Logic: Complexity and Decidability
Proc. of the 23rd Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS), 11:1--11:10, 2014. ACM

Details
Bibtex

KurzfassungAbstract
Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the model-checking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BKKW2014,
  author    = {Christel Baier and Joachim Klein and Sascha Kl{\"{u}}ppelholz and
               Sascha Wunderlich},
  title     = {Weight Monitoring with Linear Temporal Logic: Complexity and
               Decidability},
  booktitle = {Proc. of the 23rd Conference on Computer Science Logic and the
               29th Symposium on Logic In Computer Science (CSL-LICS)},
  publisher = {ACM},
  year      = {2014},
  pages     = {11:1--11:10},
  doi       = {10.1145/2603088.2603162}
}