Abstracting WS1S systems to verify parameterized networks

DOI10.1007/3-540-46419-0_14MaRDI QIDQ4518895zbMATH OpenFDO

Authors Kai Baukus, Saddek Bensalem, Karsten Stahl, Yassine Lakhnech

Publication date 5 February 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46419-0_14

zbMATH Keywords

finite state processesparameterized networksWS1S transition system

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Verification of parameterized protocols
• Verifying universal properties of parameterized networks
• Networks of processes with parameterized state space
• scientific article; zbMATH DE number 1232244
• Parameterized verification of a cache coherence protocol: Safety and liveness

Cited in

(21)

• Checking deadlock-freedom of parametric component-based systems
• Computing parameterized invariants of parameterized Petri nets
• Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
• Verification of parametric concurrent systems with prioritised FIFO resource management
• Predicate diagrams for the verification of real-time systems
• Verification of parameterized protocols
• Verifying universal properties of parameterized networks
• Monotonic extensions of Petri nets: forward and backward search revisited
• Automated formal analysis and verification: an overview
• Model-checking and abstraction to the aid of parameterized systems
• Parameterized verification of a cache coherence protocol: Safety and liveness
• Verifying a network invariant for all configurations of the Futurebus+ cache coherence protocol
• Networks of processes with parameterized state space
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Computing Parameterized Invariants of Parameterized Petri Nets
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Abduction of trap invariants in parameterized systems
• Antiprenexing for WSkS: a little goes a long way

This page was built for publication: Abstracting WS1S systems to verify parameterized networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4518895)