Bounded model checking of traffic light control system

DOI10.1016/J.ENTCS.2014.12.006MaRDI QIDQ2520617zbMATH OpenOpenAlexWikidataFDO

Authors Yanyan Li

Publication date 16 December 2016

Full work available at URL https://doi.org/10.1016/j.entcs.2014.12.006

zbMATH Keywords

verificationbounded model checkingPPTLTLCS

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Traffic problems in operations research (90B20) Temporal logic (03B44)

Recommendations

• Bounded model checking for propositional projection temporal logic
• scientific article; zbMATH DE number 1799521
• A symbolic model checker for propositional projection temporal logic
• Bounded model checking of infinite state systems
• Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 4180789 (Why is no real title available?)
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• A decision procedure for propositional projection temporal logic with infinite models
• Bounded model checking for propositional projection temporal logic
• Propositional Projection Temporal Logic, B $\ddot{u}$ chi Automata and ω-Regular Expressions
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(1)

• A canonical form based decision procedure and model checking approach for propositional projection temporal logic

Describes a project that uses

Uses Software

• NuSMV
• SPIN

This page was built for publication: Bounded model checking of traffic light control system

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