About: Abstract Regular Tree Model Checking

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

About: Abstract Regular Tree Model Checking 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	Článek zobecňuje dříve zavedenou metodu abstraktního regulárního model checkingu nad systémy s lineární (linearizovatelnou) strukturou na systémy se stromovu strukturou stavů. K representaci nekonečných množin stavů takových systémů jsou použity konečné stromové automaty. (cs) Regular (tree) model checking (RMC)  is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally Regular (tree) model checking (RMC)  is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally (en)
Title	Abstract Regular Tree Model Checking Abstract Regular Tree Model Checking (en) Abstraktní regulární model checking nad stromy (cs)
skos:prefLabel	Abstract Regular Tree Model Checking Abstract Regular Tree Model Checking (en) Abstraktní regulární model checking nad stromy (cs)
skos:notation	RIV/00216305:26230/06:PU66852!RIV07-GA0-26230___
http://linked.open.../vavai/riv/strany	37-48
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(GA102/04/0780), P(GD102/05/H050), P(GP102/03/D211)
http://linked.open...iv/cisloPeriodika	1
http://linked.open...vai/riv/dodaniDat	2007
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš Rogalewicz, Adam
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	463961
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/06:PU66852
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	formal verification, model checking, symbolic verification, regular model checking, the abstrack-check-refine paradigm, finite tree automata (en)
http://linked.open.../riv/klicoveSlovo	symbolic verification model checking regular model checking formal verification the abstrack-check-refine paradigm finite tree automata
http://linked.open...odStatuVydavatele	US - Spojené státy americké
http://linked.open...ontrolniKodProRIV	[2C0979F75BC7]
http://linked.open...i/riv/nazevZdroje	ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems Integrated Approach to Education of PhD Students in the Area of Parallel and Distributed Systems Automated methods and tools supporting development of reliable concurrent and distributed systems
http://linked.open...UplatneniVysledku	2006
http://linked.open...v/svazekPeriodika	149
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Habermehl, Peter Rogalewicz, Adam Bouajjani, Ahmed
issn	1571-0661
number of pages	12 (xsd:int)
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Abstract Regular Tree Model Checking Abstract Regular Tree Model Checking

Faceted Search & Find service v1.16.116 as of Feb 22 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

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