About: Deciding bisimulation-likeequivalences with finite-state processes

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

About: Deciding bisimulation-likeequivalences with finite-state processes 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	We show that characteristic formulae for finite-state systems up to bisimulation-like equivalences (e.g., strong and weak bisimilarity) can be given in the simple branching-time temporal logic EF. Since EF is a very weak fragment of the modal mu-calculus, model checking with EF is decidable for many more classes of infinite-state systems. This yields a general method for proving decidability of bisimulation-like equivalences between infinite-state processes and finite-state ones. We apply this method tothe class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showing that a large class of bisimulation-like equivalences (including, e.g., strong and weak bisimilarity) is decidable between PAD and finite-state processes. On the other hand, we also demonstrate that no `reasonable' bisimulation-like equivalence is decidable between state-extended PA processes and finite-state ones. Furthermore, weak bisimilarity with finite-state processes is shown to be undecidable even for sta We show that characteristic formulae for finite-state systems up to bisimulation-like equivalences (e.g., strong and weak bisimilarity) can be given in the simple branching-time temporal logic EF. Since EF is a very weak fragment of the modal mu-calculus, model checking with EF is decidable for many more classes of infinite-state systems. This yields a general method for proving decidability of bisimulation-like equivalences between infinite-state processes and finite-state ones. We apply this method tothe class of PAD processes, which strictly subsumes PA and pushdown (PDA) processes, showing that a large class of bisimulation-like equivalences (including, e.g., strong and weak bisimilarity) is decidable between PAD and finite-state processes. On the other hand, we also demonstrate that no `reasonable' bisimulation-like equivalence is decidable between state-extended PA processes and finite-state ones. Furthermore, weak bisimilarity with finite-state processes is shown to be undecidable even for sta (en)
Title	Deciding bisimulation-likeequivalences with finite-state processes Deciding bisimulation-likeequivalences with finite-state processes (en)
skos:prefLabel	Deciding bisimulation-likeequivalences with finite-state processes Deciding bisimulation-likeequivalences with finite-state processes (en)
skos:notation	RIV/61989100:27240/01:00001048!RIV/2002/GA0/272402/N
http://linked.open.../vavai/riv/strany	409-433
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(GA201/97/0456), P(GA201/98/P046), Z(MSM 143300001), Z(MSM 272400013)
http://linked.open...iv/cisloPeriodika	258
http://linked.open...vai/riv/dodaniDat	2002
http://linked.open...aciTvurceVysledku	Jančar, Petr
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á škola báňská - Technická univerzita Ostrava / Fakulta elektrotechniky a informatiky
http://linked.open...dnocenehoVysledku	676970
http://linked.open...ai/riv/idVysledku	RIV/61989100:27240/01:00001048
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	concurrency; bisimulation; characteristic formulae; infinite-state systems (en)
http://linked.open.../riv/klicoveSlovo	concurrency infinite-state systems bisimulation characteristic formulae
http://linked.open...odStatuVydavatele	BE - Belgické království
http://linked.open...ontrolniKodProRIV	[503ED1E62C5B]
http://linked.open...i/riv/nazevZdroje	Theoretical Computer Science
http://linked.open...in/vavai/riv/obor	BD
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...ocetUcastnikuAkce	0 (xsd:int)
http://linked.open...nichUcastnikuAkce	0 (xsd:int)
http://linked.open...vavai/riv/projekt	Algorithmic verification boundaries for infinite-state systems Decidability Issues for process algebras
http://linked.open...UplatneniVysledku	2001
http://linked.open...v/svazekPeriodika	Neuveden
http://linked.open...iv/tvurceVysledku	Jančar, Petr Kučera, A. Mayr, R.
http://linked.open...n/vavai/riv/zamer	http://linked.opendata.cz/resource/domain/vavai/zamer/MSM%20143300001 http://linked.opendata.cz/resource/domain/vavai/zamer/MSM%20272400013
issn	0304-3975
number of pages	24 (xsd:int)
http://localhost/t...ganizacniJednotka	27240

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, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software