GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic

DOI10.1007/978-3-540-78800-3_26MaRDI QIDQ5458337zbMATH OpenOpenAlexFDO

Authors Yih-Kuen Tsay, Yu-Fang Chen, Ming-Hsien Tsai, Wen-Chin Chan, Chi-Jian Luo

Publication date 11 April 2008

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78800-3_26

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1863182
• scientific article; zbMATH DE number 1424021
• Owl: a library for \(\omega \)-words, automata, and LTL
• Implementation and Application of Automata
• Experiments with deterministic -automata for formulas of linear temporal logic

Cites work

• ``More deterministic vs. ``smaller Büchi automata for efficient LTL model checking
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 1973991 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 2102710 (Why is no real title available?)
• scientific article; zbMATH DE number 1408338 (Why is no real title available?)
• Mathematical Foundations of Computer Science 2003
• Nested emptiness search for generalized Büchi automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification by augmented finitary abstraction
• Weak alternating automata are not that weak

Cited in

(7)

• Tool support for learning Büchi automata and linear temporal logic
• A theoretical framework for cardinality-based feature models: the semantics and computational aspects
• Büchi Store: an open repository of Büchi automata
• State of Büchi complementation
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• From linear temporal logics to Büchi automata: the early and simple principle
• Owl: a library for \(\omega \)-words, automata, and LTL

Describes a project that uses

Uses Software

• LTL2BA

This page was built for publication: GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic

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