About: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking. The paper considers several issues related to efficient use of tree automata in formal verification. First, a new efficient algorithm for inclusion checking on non-deterministic tree automata is proposed. The algorithm traverses the automaton downward, utilizing antichains and simulations to optimize its run. Results of a set of experiments are provided, showing that such an approach often very significantly outperforms the so far common upward inclusion checking. Next, a new semi-symbolic representation of non-deterministic tree automata, suitable for automata with huge alphabets, is proposed together with algorithms for upward as well as downward inclusion checking over this representation of tree automata. Results of a set of experiments comparing the performance of these algorithms are provided, again showing that the newly proposed downward inclusion is very often better than upward inclusion checking. (en)
Title	Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata (en)
skos:prefLabel	Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata (en)
skos:notation	RIV/00216305:26230/11:PU96118!RIV12-MSM-26230___
http://linked.open...avai/predkladatel	Fakulta informačních technologií
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(GAP103/10/0306), P(GD102/09/H042), P(OC10009), S, Z(MSM0021630528)
http://linked.open...iv/cisloPeriodika	6996
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Lengál, Ondřej Šimáček, Jiří Holík, Lukáš Vojnar, Tomáš
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	196752
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/11:PU96118
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	tree automata, binary decision diagrams, language inclusion, downward inclusion checking, symbolic encoding (en)
http://linked.open.../riv/klicoveSlovo	binary decision diagrams downward inclusion checking language inclusion symbolic encoding tree automata
http://linked.open...odStatuVydavatele	DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV	[EDB7919E21CF]
http://linked.open...i/riv/nazevZdroje	Lecture Notes in Computer Science (IF 0,513)
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	4 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
http://linked.open...UplatneniVysledku	2011
http://linked.open...v/svazekPeriodika	2011
http://linked.open...iv/tvurceVysledku	Holík, Lukáš Vojnar, Tomáš Lengál, Ondřej Šimáček, Jiří
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
issn	0302-9743
number of pages	16 (xsd:int)
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 47 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software