Linear temporal logic symbolic model checking (Q465680): Difference between revisions

@@ Property / author @@
-Kristin Yvonne Rozier
@@ Property / author: Kristin Yvonne Rozier / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+HyTech
@@ Property / describes a project that uses: HyTech / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+NuSMV
@@ Property / describes a project that uses: NuSMV / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VIS
@@ Property / describes a project that uses: VIS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPOT
@@ Property / describes a project that uses: SPOT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LTL2BA
@@ Property / describes a project that uses: LTL2BA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SPIN
@@ Property / describes a project that uses: SPIN / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Uppaal
@@ Property / describes a project that uses: Uppaal / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Java PathFinder
@@ Property / describes a project that uses: Java PathFinder / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cadence SMV
@@ Property / describes a project that uses: Cadence SMV / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CESAR
@@ Property / describes a project that uses: CESAR / rank @@
+Normal rank
@@ Property / author @@
+Kristin Yvonne Rozier
@@ Property / author: Kristin Yvonne Rozier / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.cosrev.2010.06.002
+Normal rank
@@ Property / OpenAlex ID @@
+W1965024948
@@ Property / OpenAlex ID: W1965024948 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3336675
@@ Property / cites work: Q3336675 / rank @@
+Normal rank
@@ Property / cites work @@
+SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR
+Normal rank
@@ Property / cites work @@
+Automata-Theoretic Model Checking Revisited
@@ Property / cites work: Automata-Theoretic Model Checking Revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Q4356435
@@ Property / cites work: Q4356435 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2747613
@@ Property / cites work: Q2747613 / rank @@
+Normal rank
@@ Property / cites work @@
+Model Checking Software
@@ Property / cites work: Model Checking Software / rank @@
+Normal rank
@@ Property / cites work @@
+NuSMV: A new symbolic model checker
@@ Property / cites work: NuSMV: A new symbolic model checker / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic model checking: \(10^{20}\) states and beyond
+Normal rank
@@ Property / cites work @@
+The Birth of Model Checking
@@ Property / cites work: The Birth of Model Checking / rank @@
+Normal rank
@@ Property / cites work @@
+Q4037380
@@ Property / cites work: Q4037380 / rank @@
+Normal rank
@@ Property / cites work @@
+HyTech: A model checker for hybrid systems
@@ Property / cites work: HyTech: A model checker for hybrid systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754072
@@ Property / cites work: Q2754072 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4531751
@@ Property / cites work: Q4531751 / rank @@
+Normal rank
@@ Property / cites work @@
+Correct Hardware Design and Verification Methods
@@ Property / cites work: Correct Hardware Design and Verification Methods / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Technology for Verification and Analysis
+Normal rank
@@ Property / cites work @@
+Q2852018
@@ Property / cites work: Q2852018 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804909
@@ Property / cites work: Q4804909 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q4054648
@@ Property / cites work: Q4054648 / rank @@
+Normal rank
@@ Property / cites work @@
+LAR: A logic of algorithmic reasoning
@@ Property / cites work: LAR: A logic of algorithmic reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+From Church and Prior to PSL
@@ Property / cites work: From Church and Prior to PSL / rank @@
+Normal rank
@@ Property / cites work @@
+Practical CTL* model checking: Should SPIN be extended?
+Normal rank
@@ Property / cites work @@
+Q4385542
@@ Property / cites work: Q4385542 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2771059
@@ Property / cites work: Q2771059 / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic verification of finite-state concurrent systems using temporal logic specifications
+Normal rank
@@ Property / cites work @@
+Reasoning about infinite computations
@@ Property / cites work: Reasoning about infinite computations / rank @@
+Normal rank
@@ Property / cites work @@
+The complexity of propositional linear temporal logics
+Normal rank
@@ Property / cites work @@
+Propositional dynamic logic of regular programs
@@ Property / cites work: Propositional dynamic logic of regular programs / rank @@
+Normal rank
@@ Property / cites work @@
+Decision procedures and expressiveness in the temporal logic of branching time
+Normal rank
@@ Property / cites work @@
+Q4936139
@@ Property / cites work: Q4936139 / rank @@
+Normal rank
@@ Property / cites work @@
+Logic in Computer Science
@@ Property / cites work: Logic in Computer Science / rank @@
+Normal rank
@@ Property / cites work @@
+Q5322945
@@ Property / cites work: Q5322945 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2733893
@@ Property / cites work: Q2733893 / rank @@
+Normal rank
@@ Property / cites work @@
+“Sometimes” and “not never” revisited
@@ Property / cites work: “Sometimes” and “not never” revisited / rank @@
+Normal rank
@@ Property / cites work @@
+Deciding full branching time logic
@@ Property / cites work: Deciding full branching time logic / rank @@
+Normal rank
@@ Property / cites work @@
+Temporal logic can be more expressive
@@ Property / cites work: Temporal logic can be more expressive / rank @@
+Normal rank
@@ Property / cites work @@
+The complementation problem for Büchi automata with applications to temporal logic
+Normal rank
@@ Property / cites work @@
+Q4472249
@@ Property / cites work: Q4472249 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4551164
@@ Property / cites work: Q4551164 / rank @@
+Normal rank
@@ Property / cites work @@
+From Monadic Logic to PSL
@@ Property / cites work: From Monadic Logic to PSL / rank @@
+Normal rank
@@ Property / cites work @@
+Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
+Normal rank
@@ Property / cites work @@
+Towards a general theory of action and time
@@ Property / cites work: Towards a general theory of action and time / rank @@
+Normal rank
@@ Property / cites work @@
+Sanity Checks in Formal Verification
@@ Property / cites work: Sanity Checks in Formal Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient detection of vacuity in temporal model checking
+Normal rank
@@ Property / cites work @@
+Correct Hardware Design and Verification Methods
@@ Property / cites work: Correct Hardware Design and Verification Methods / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Formal Methods in Computer-Aided Design
@@ Property / cites work: Formal Methods in Computer-Aided Design / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q4804918
@@ Property / cites work: Q4804918 / rank @@
+Normal rank
@@ Property / cites work @@
+An automata-theoretic approach to branching-time model checking
+Normal rank
@@ Property / cites work @@
+Q5525343
@@ Property / cites work: Q5525343 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4493881
@@ Property / cites work: Q4493881 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3698787
@@ Property / cites work: Q3698787 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4817549
@@ Property / cites work: Q4817549 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754087
@@ Property / cites work: Q2754087 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4551134
@@ Property / cites work: Q4551134 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4422087
@@ Property / cites work: Q4422087 / rank @@
+Normal rank
@@ Property / cites work @@
+Correct Hardware Design and Verification Methods
@@ Property / cites work: Correct Hardware Design and Verification Methods / rank @@
+Normal rank
@@ Property / cites work @@
+Concepts of Automata Construction from LTL
@@ Property / cites work: Concepts of Automata Construction from LTL / rank @@
+Normal rank
@@ Property / cites work @@
+Proving the Correctness of Multiprocess Programs
@@ Property / cites work: Proving the Correctness of Multiprocess Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Liveness Properties of Concurrent Programs
+Normal rank
@@ Property / cites work @@
+Q4817542
@@ Property / cites work: Q4817542 / rank @@
+Normal rank
@@ Property / cites work @@
+Recognizing safety and liveness
@@ Property / cites work: Recognizing safety and liveness / rank @@
+Normal rank
@@ Property / cites work @@
+Safety, liveness and fairness in temporal logic
@@ Property / cites work: Safety, liveness and fairness in temporal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Defining liveness
@@ Property / cites work: Defining liveness / rank @@
+Normal rank
@@ Property / cites work @@
+Weak alternating automata are not that weak
@@ Property / cites work: Weak alternating automata are not that weak / rank @@
+Normal rank
@@ Property / cites work @@
+Improved Algorithms for the Automata-Based Approach to Model-Checking
+Normal rank
@@ Property / cites work @@
+Büchi Complementation and Size-Change Termination
+Normal rank
@@ Property / cites work @@
+Q5628016
@@ Property / cites work: Q5628016 / rank @@
+Normal rank
@@ Property / cites work @@
+Binary Decision Diagrams
@@ Property / cites work: Binary Decision Diagrams / rank @@
+Normal rank
@@ Property / cites work @@
+Q4160379
@@ Property / cites work: Q4160379 / rank @@
+Normal rank
@@ Property / cites work @@
+Graph-Based Algorithms for Boolean Function Manipulation
+Normal rank
@@ Property / cites work @@
+Q3992994
@@ Property / cites work: Q3992994 / rank @@
+Normal rank
@@ Property / cites work @@
+Decidability of model checking for infinite-state concurrent systems
+Normal rank
@@ Property / cites work @@
+Reduction of OBDDs in linear time
@@ Property / cites work: Reduction of OBDDs in linear time / rank @@
+Normal rank
@@ Property / cites work @@
+Propositional dynamic logic of looping and converse is elementarily decidable
+Normal rank
@@ Property / cites work @@
+A new heuristic for bad cycle detection using BDDs
+Normal rank
@@ Property / cites work @@
+An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
+Normal rank
@@ Property / cites work @@
+Q2771062
@@ Property / cites work: Q2771062 / rank @@
+Normal rank
@@ Property / cites work @@
+The nonapproximability of OBDD minimization
@@ Property / cites work: The nonapproximability of OBDD minimization / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:465680