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

From LRDE

Line 10: Line 10:
 
| 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. lrdekeywords = Spot
+
| 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
 
| lrdenewsdate = 2020-07-07
 
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf
 
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renkin.20.atva.pdf

Revision as of 09:41, 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.

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