A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems

DOI10.1093/LOGCOM/2.5.605MaRDI QIDQ5285990zbMATH OpenOpenAlexFDO

Authors Orna Grumberg, Edmund Clarke, R. P. Kurshan

Publication date 29 June 1993

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/2.5.605

zbMATH Keywords

model checkingtemporal logics\(\omega\)-regular languagesfinite-state systemsautomata on infinite tapes

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 4128366
• scientific article; zbMATH DE number 3932379
• Automatic verification methods for finite state systems. International workshop, Grenoble, France, June 12-14, 1989. Proceedings

Cited in

(7)

• Stepwise refinement and concurrency: The finite-state case
• Stochastic game logic
• Proving Liveness and Termination of Systolic Arrays Using Communicating Finite State Machines
• scientific article; zbMATH DE number 4128366 (Why is no real title available?)
• Verification of reactive systems using temporal logic with clocks
• Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
• Automatic verification of finite-state concurrent systems using temporal logic specifications

This page was built for publication: A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems

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