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

From LRDE

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}
}