About: Advanced Ramsey-based Büchi Automata Inclusion Testing

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

About: Advanced Ramsey-based Büchi Automata Inclusion Testing 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	Checking language inclusion between two nondeterministic Büchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from Checking language inclusion between two nondeterministic Büchi automata A and B is computationally hard (PSPACE-complete). However, several approaches which are efficient in many practical cases have been proposed. We build on one of these, which is known as the Ramsey-based approach. It has recently been shown that the basic Ramsey-based approach can be drastically optimized by using powerful subsumption techniques, which allow one to prune the search-space when looking for counterexamples to inclusion. While previous works only used subsumption based on set inclusion or forward simulation on A and B, we propose the following new techniques: (1) A larger subsumption relation based on a combination of backward and forward simulations on A and B. (2) A method to additionally use forward simulation between A and B. (3) Abstraction techniques that can speed up the computation and lead to early detection of counterexamples. The new algorithm was implemented and tested on automata derived from (en)
Title	Advanced Ramsey-based Büchi Automata Inclusion Testing Advanced Ramsey-based Büchi Automata Inclusion Testing (en)
skos:prefLabel	Advanced Ramsey-based Büchi Automata Inclusion Testing Advanced Ramsey-based Büchi Automata Inclusion Testing (en)
skos:notation	RIV/00216305:26230/11:PU96126!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	6901
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	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	184741
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/11:PU96126
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Büchi automata, inclusion checking, Ramsey theorem, simulation relations (en)
http://linked.open.../riv/klicoveSlovo	Büchi automata Ramsey theorem inclusion checking simulation relations
http://linked.open...odStatuVydavatele	DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV	[06A777AF9607]
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	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	7 (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	Abdulla, Parosh Chen, Yu-Fang Clemente, Lorenzo Holík, Lukáš Hong, Chih-Duo Mayr, Richard Vojnar, Tomáš
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	Advanced Ramsey-based Büchi Automata Inclusion Testing Advanced Ramsey-based Büchi Automata Inclusion Testing

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