Verifying specifications in the language L against temporal properties nonexpressible in this language

DOI10.1007/s10559-009-9140-2zbMath1185.68410OpenAlexW2032155506MaRDI QIDQ844345

Anatoli N. Chebotarev

Publication date: 19 January 2010

Published in: Cybernetics and Systems Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10559-009-9140-2

zbMATH Keywords

verificationopen systemlanguage \(GR(1)\)reactive algorithmspecification language Lsuperwordstemporal property

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Unnamed Item
• Unnamed Item
• Approach to functional specification of automaton systems. I
• Consistency test for simple specifications of automaton systems
• Separable resolution method for checking the satisfiability of formulas in the language \({\mathfrak L}\)
• Checking the satisfiability of formulas represented in disjunctive normal form in the language \(L\). I
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Verifying specifications in the language L against temporal properties nonexpressible in this language