vix.ing · top · new · best · stats · spec

Branching Bisimilarity Checking for PRS

2014/02/01 by Qiang Yin, Yuxi Fu, Yin, Qiang +7
Computer Science · #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling

paper · pdf · doi:10.48550/arxiv.1402.0050

openalex publication_date 2014/02/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/04

Abstract

Recent studies reveal that branching bisimilarity is decidable for both nBPP (normed Basic Parallel Process) and nBPA (normed Basic Process Algebra). These results lead to the question if there are any other models in the hierarchy of PRS (Process Rewrite System) whose branching bisimilarity is decidable. It is shown in this paper that the branching bisimilarity for both nOCN (normed One Counter Net) and nPA (normed Process Algebra) is undecidable. These results essentially imply that the question has a negative answer.

Citations

Related