Streett Automata Model Checking of Higher-Order Recursion Schemes

DOI10.4230/LIPICS.FSCD.2017.32zbMATH Open1441.68135OpenAlexW3170373610MaRDI QIDQ5111330FDOQ5111330

Takeshi Tsukada, Koichi Fujima, Naoki Kobayashi, Ryota Suzuki

Publication date: 26 May 2020

Full work available at URL: https://cir.nii.ac.jp/ja/crid/1010282202008768001

zbMATH Keywords

higher-order model checkinghigher-order recursion schemesStreett automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Automata, logics, and infinite games. A guide to current research
• Propositional dynamic logic of looping and converse is elementarily decidable
• Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata
• Types and higher-order recursion schemes for verification of higher-order programs
• Typed Lambda Calculi and Applications
• A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes
• Model Checking Higher-Order Programs
• Verification of concurrent programs: The automata-theoretic framework
• Proving that programs eventually do something good
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Verifying higher-order functional programs with pattern-matching algebraic data types
• On the complexity of set-based analysis
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• A type-directed abstraction refinement approach to higher-order model checking
• Automatically disproving fair termination of higher-order functional programs
• Relational semantics of linear logic and higher-order model-checking
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Tractable constraints in finite semilattices
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Temporal verification of higher-order functional programs
• Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• A traversal-based algorithm for higher-order model checking
• Finitary Semantics of Linear Logic and Higher-Order Model-Checking
• Compositional higher-order model checking via ω -regular games over Böhm trees

Cited In (6)

• Exact bounds for acyclic higher-order recursion schemes
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Title not available (Why is that?)
• A type-based HFL model checking algorithm
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Generalizations of checking stack automata: characterizations and hierarchies

Uses Software

• TravMC
• TravMC2
• MoCHi
• GitHub

   Recommendations

• Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes 👍 👎
• Saturation-Based Model Checking of Higher-Order Recursion Schemes. 👍 👎
• A traversal-based algorithm for higher-order model checking 👍 👎
• A Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes 👍 👎
• Model-Checking Higher-Order Programs with Recursive Types 👍 👎

This page was built for publication: Streett Automata Model Checking of Higher-Order Recursion Schemes

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