A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
From MaRDI portal
Publication:3636802
DOI10.2168/LMCS-5(2:3)2009zbMATH Open1163.68030arXiv0903.3126OpenAlexW3102946820MaRDI QIDQ3636802FDOQ3636802
Authors: Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Yan Jurski, Mihaela Sighireanu 
Publication date: 30 June 2009
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens. We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.
Full work available at URL: https://arxiv.org/abs/0903.3126
Recommendations
Cited In (2)
This page was built for publication: A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3636802)
