Difference between revisions of "Publications/renkin.20.atva"

From LRDE

(Created page with "{{Publication | published = true | date = 2020-10-01 | authors = Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet | title = Practical “Paritizing” of Emerson-Lei Aut...")
 
Line 1: Line 1:
 
{{Publication
 
{{Publication
 
| published = true
 
| published = true
| date = 2020-10-01
+
| date = 2020-07-07
 
| authors = Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet
 
| authors = Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet
 
| title = Practical “Paritizing” of Emerson-Lei Automata
 
| title = Practical “Paritizing” of Emerson-Lei Automata
Line 8: Line 8:
 
| series = Lecture Notes in Computer Science
 
| series = Lecture Notes in Computer Science
 
| pages = ??? to ???
 
| pages = ??? to ???
| lrdeprojects = Spot
 
 
| publisher = Springer
 
| publisher = Springer
 
| note = To appear
 
| note = To appear
| abstract = We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an <math>\omega</math>-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a emphlatest appearance record principle, and introduces a emphpartial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.
+
| abstract = We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an <math>\omega</math>-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a emphlatest appearance record principle, and introduces a emphpartial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. lrdekeywords = Spot
  +
| lrdenewsdate = 2020-07-07
  +
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf
 
| type = inproceedings
 
| type = inproceedings
 
| id = renkin.20.atva
 
| id = renkin.20.atva

Revision as of 09:35, 7 July 2020

Abstract

We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an -automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a emphlatest appearance record principle, and introduces a emphpartial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step. lrdekeywords = Spot

Documents

Bibtex (lrde.bib)

@InProceedings{	  renkin.20.atva,
  author	= {Florian Renkin and Alexandre Duret-Lutz and Adrien
		  Pommellet},
  title		= {Practical ``Paritizing'' of Emerson-Lei Automata},
  booktitle	= {Proceedings of the 18th International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'20)},
  year		= {2020},
  volume	= {?????},
  series	= {Lecture Notes in Computer Science},
  pages		= {???--???},
  month		= oct,
  publisher	= {Springer},
  note		= {To appear},
  abstract	= {We introduce a new algorithm that takes a
		  \emph{Transition-based Emerson-Lei Automaton} (TELA), that
		  is, an $\omega$-automaton whose acceptance condition is an
		  arbitrary Boolean formula on sets of transitions to be seen
		  infinitely or finitely often, and converts it into a
		  \emph{Transition-based Parity Automaton} (TPA). To reduce
		  the size of the output TPA, the algorithm combines and
		  optimizes two procedures based on a \emph{latest appearance
		  record} principle, and introduces a \emph{partial
		  degeneralization}. Our motivation is to use this algorithm
		  to improve our LTL synthesis tool, where producing
		  deterministic parity automata is an intermediate step.}
}