About: Undecidability of bisimilarity by Defender's forcing

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

About: Undecidability of bisimilarity by Defender's forcing 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	Stirling (1996, 1998) proved the decidability of bisimilarity on so called normed pushdown processes. This result was substantially extended by Senizergues (1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the epsilon-transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted epsilon-popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, i.e., we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. Stirling (1996, 1998) proved the decidability of bisimilarity on so called normed pushdown processes. This result was substantially extended by Senizergues (1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the epsilon-transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted epsilon-popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, i.e., we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. (en)
Title	Undecidability of bisimilarity by Defender's forcing Undecidability of bisimilarity by Defender's forcing (en)
skos:prefLabel	Undecidability of bisimilarity by Defender's forcing Undecidability of bisimilarity by Defender's forcing (en)
skos:notation	RIV/61989100:27240/08:00018940!RIV11-MSM-27240___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(1M0567), Z(MSM0021622419)
http://linked.open...iv/cisloPeriodika	1
http://linked.open...vai/riv/dodaniDat	2011
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	401421
http://linked.open...ai/riv/idVysledku	RIV/61989100:27240/08:00018940
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	bisimilarity, pushdown automata, process algebra, undecidability (en)
http://linked.open.../riv/klicoveSlovo	process algebra bisimilarity pushdown automata undecidability
http://linked.open...odStatuVydavatele	US - Spojené státy americké
http://linked.open...ontrolniKodProRIV	[6E48ED8C9A05]
http://linked.open...i/riv/nazevZdroje	Journal of the ACM
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	Centre for Applied Cybernetics
http://linked.open...UplatneniVysledku	2008
http://linked.open...v/svazekPeriodika	55
http://linked.open...iv/tvurceVysledku	Srba, Jiří Jančar, Petr
http://linked.open...ain/vavai/riv/wos	000253939800005
http://linked.open...n/vavai/riv/zamer	Highly Parallel and Distributed Computing Systems
issn	0004-5411
number of pages	27 (xsd:int)
http://localhost/t...ganizacniJednotka	27240
is http://linked.open...avai/riv/vysledek of	Undecidability of bisimilarity by Defender's forcing Undecidability of bisimilarity by Defender's forcing Undecidability of bisimilarity by Defender's forcing

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