2014/02/11 by Mateus de Oliveira Oliveira, Oliveira, Mateus de Oliveira
Computer Science · #Data Structures and Algorithms (cs.DS) #Distributed #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Parallel #Petri Nets in System Modeling #and Cluster Computing (cs.DC) #cs.DC #cs.DS #cs.LO
paper · pdf · doi:10.48550/arxiv.1402.2698
arxiv created 2014/02/11 · openalex publication_date 2014/02/11 · arxiv updated 2014/02/14 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
In this work we provide algorithmic solutions to five fundamental problems concerning the verification, synthesis and correction of concurrent systems that can be modeled by bounded p/t-nets. We express concurrency via partial orders and assume that behavioral specifications are given via monadic second order logic. A c-partial-order is a partial order whose Hasse diagram can be covered by c paths. For a finite set T of transitions, we let P(c,T,ϕ) denote the set of all T-labelled c-partial-orders satisfying ϕ. If N=(P,T) is a p/t-net we let P(N,c) denote the set of all c-partially-ordered runs of N. A (b, r)-bounded p/t-net is a b-bounded p/t-net in which each place appears repeated at most r times. We solve the following problems: 1. Verification: given an MSO formula ϕand a bounded p/t-net N determine whether P(N,c)⊆ P(c,T,ϕ), whether P(c,T,ϕ)⊆ P(N,c), or whether P(N,c)∩ P(c,T,ϕ)=∅. 2. Synthesis from MSO Specifications: given an MSO formula ϕ, synthesize a semantically minimal (b,r)-bounded p/t-net N satisfying P(c,T,ϕ)⊆ P(N, c). 3. Semantically Safest Subsystem: given an MSO formula ϕdefining a set of safe partial orders, and a b-bounded p/t-net N, possibly containing unsafe behaviors, synthesize the safest (b,r)-bounded p/t-net N' whose behavior lies in between P(N,c)∩ P(c,T,ϕ) and P(N,c). 4. Behavioral Repair: given two MSO formulas ϕand ψ, and a b-bounded p/t-net N, synthesize a semantically minimal (b,r)-bounded p/t net N' whose behavior lies in between P(N,c) ∩ P(c,T,ϕ) and P(c,T,ψ). 5. Synthesis from Contracts: given an MSO formula ϕyes specifying a set of good behaviors and an MSO formula ϕno specifying a set of bad behaviors, synthesize a semantically minimal (b,r)-bounded p/t-net N such that P(c,T,ϕyes) ⊆ P(N,c) but P(c,T,ϕno ) ∩ P(N,c)=∅.