Difference between revisions of "Publications/dziadek.23.fm"

From LRDE

Line 10: Line 10:
 
| 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.
 
| 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.
 
| lrdenewsdate = 2022-12-08
 
| lrdenewsdate = 2022-12-08
  +
| note = Accepted
 
| type = inproceedings
 
| type = inproceedings
 
| id = dziadek.23.fm
 
| id = dziadek.23.fm
Line 31: Line 32:
 
relying on the corner-point abstraction. All our algorithms
 
relying on the corner-point abstraction. All our algorithms
 
are freely available and implemented in a tool based on the
 
are freely available and implemented in a tool based on the
open-source tools TChecker and Spot.<nowiki>}</nowiki>
+
open-source tools TChecker and Spot.<nowiki>}</nowiki>,
  +
note = <nowiki>{</nowiki>Accepted<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
 
<nowiki>}</nowiki>
   

Revision as of 09:49, 21 December 2022

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