On the Model Checking Problem for Some Extension of CTL*

DOI10.18255/1818-1015-2020-4-428-441MaRDI QIDQ5060078zbMATH OpenOpenAlexFDO

Authors Anton Romanovich Gnatenko, Vladimir A. Zakharov

Publication date 17 January 2023

Published in Modeling and Analysis of Information Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL http://mathnet.ru/eng/mais726

zbMATH Keywords

finite-state transducermodel checkingreactive systemregular languagespecificationtemporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model checking of RegCTL
• Local distributed model checking of RegCTL
• Extended computation tree logic
• scientific article; zbMATH DE number 2196601
• \(\infty\)-regular temporal logic and its model checking problem

Cites work

• CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
• Dynamic linear time temporal logic
• scientific article; zbMATH DE number 3876574 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3767031 (Why is no real title available?)
• scientific article; zbMATH DE number 1836373 (Why is no real title available?)
• scientific article; zbMATH DE number 1863182 (Why is no real title available?)
• Model checking
• Regular Linear Temporal Logic
• Relationships between nondeterministic and deterministic tape complexities
• Streaming transducers for algorithmic verification of single-pass list-processing programs
• Symbolic finite state transducers: algorithms and applications
• Temporal logic can be more expressive

Cited in

(10)

• Specification and verification of decentralized daisy chain arbiters with \(\omega\)-extended regular expressions
• \(\infty\)-regular temporal logic and its model checking problem
• Model checking CTL over restricted classes of automatic structures
• Model checking temporal properties of reaction systems
• Local distributed model checking of RegCTL
• Model checking of RegCTL
• scientific article; zbMATH DE number 1927565 (Why is no real title available?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Automated Technology for Verification and Analysis
• On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

This page was built for publication: On the Model Checking Problem for Some Extension of CTL*

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