Attributes | Values |
---|
rdf:type
| |
Description
| - We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Büchi automata studied in this context and we indicate possible applications.
- We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Büchi automata studied in this context and we indicate possible applications. (en)
|
Title
| - Almost Linear Büchi Automata
- Almost Linear Büchi Automata (en)
|
skos:prefLabel
| - Almost Linear Büchi Automata
- Almost Linear Büchi Automata (en)
|
skos:notation
| - RIV/00216224:14330/09:00029631!RIV10-GA0-14330___
|
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| - P(1M0545), P(GP201/08/P375), P(GP201/08/P459), Z(MSM0021622419)
|
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216224:14330/09:00029631
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - LTL; linear time logic; model checking (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...v/mistoKonaniAkce
| |
http://linked.open...i/riv/mistoVydani
| |
http://linked.open...i/riv/nazevZdroje
| - Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09)
|
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...vavai/riv/projekt
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...iv/tvurceVysledku
| - Řehák, Vojtěch
- Babiak, Tomáš
- Strejček, Jan
|
http://linked.open...vavai/riv/typAkce
| |
http://linked.open.../riv/zahajeniAkce
| |
http://linked.open...n/vavai/riv/zamer
| |
issn
| |
number of pages
| |
http://purl.org/ne...btex#hasPublisher
| |
http://localhost/t...ganizacniJednotka
| |
is http://linked.open...avai/riv/vysledek
of | |