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

From LRDE

Line 13: Line 13:
 
| type = inproceedings
 
| type = inproceedings
 
| id = dziadek.23.fm
 
| id = dziadek.23.fm
| identifier = doi:
+
| identifier = doi:FIXME
 
| bibtex =
 
| bibtex =
 
@InProceedings<nowiki>{</nowiki> dziadek.23.fm,
 
@InProceedings<nowiki>{</nowiki> dziadek.23.fm,
Line 25: Line 25:
 
year = 2023,
 
year = 2023,
 
month = mar,
 
month = mar,
doi = <nowiki>{</nowiki><nowiki>}</nowiki>,
+
doi = <nowiki>{</nowiki>FIXME<nowiki>}</nowiki>,
 
abstract = <nowiki>{</nowiki>We show how to efficiently solve energy B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi problems
 
abstract = <nowiki>{</nowiki>We show how to efficiently solve energy B<nowiki>{</nowiki>\"u<nowiki>}</nowiki>chi problems
 
in finite weighted automata and in one-clock weighted timed
 
in finite weighted automata and in one-clock weighted timed

Revision as of 19:07, 7 April 2023

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		= {FIXME},
  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}
}