Energy Problems in Finite and Timed Automata with Büchi Conditions

Authors

Sven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier

Where

International Symposium on Formal Methods (FM)

Type

inproceedings

Publisher

Springer

Projects

AA"AA" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property., Spot

Date

2022-12-08

Abstract

We show how to efficiently solve energy Büchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford interleaved with Couvreur's algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source tools TChecker and Spot.

Bibtex (lrde.bib)

@InProceedings{	  dziadek.23.fm,
  author	= {Sven Dziadek and Uli Fahrenberg and Philipp
		  Schlehuber-Caissier},
  title		= {Energy Problems in Finite and Timed Automata with
		  {B{\"u}chi} Conditions},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  booktitle	= {International Symposium on Formal Methods (FM)},
  year		= 2023,
  month		= mar,
  doi		= {10.1007/978-3-031-27481-7_14},
  abstract	= {We show how to efficiently solve energy B{\"u}chi problems
		  in finite weighted automata and in one-clock weighted timed
		  automata. Solving the former problem is our main
		  contribution and is handled by a modified version of
		  Bellman-Ford interleaved with Couvreur's algorithm. The
		  latter problem is handled via a reduction to the former
		  relying on the corner-point abstraction. All our algorithms
		  are freely available and implemented in a tool based on the
		  open-source tools TChecker and Spot.},
  note		= {Accepted}
}