scientific article
From MaRDI portal
Publication:2754087
zbMath0974.68086MaRDI QIDQ2754087
Publication date: 11 November 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (41)
From LTL to deterministic automata. A safraless compositional approach ⋮ Good-for-MDPs Automata for Probabilistic Analysis and Reinforcement Learning ⋮ Applicability of fair simulation ⋮ Automata Theory and Model Checking ⋮ Graph Games and Reactive Synthesis ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ From LTL to unambiguous Büchi automata via disambiguation of alternating automata ⋮ Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL ⋮ GSTE is partitioned model checking ⋮ Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic ⋮ Logic programming approach to automata-based decision procedures ⋮ LTL under reductions with weaker conditions than stutter invariance ⋮ Index appearance record with preorders ⋮ On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ Markov chains and unambiguous automata ⋮ Simulation relations and applications in formal methods ⋮ Finding and fixing faults ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ LTL to self-loop alternating automata with generic acceptance and back ⋮ Unnamed Item ⋮ Antichains and compositional algorithms for LTL synthesis ⋮ Linear temporal logic symbolic model checking ⋮ Büchi Store: An Open Repository of Büchi Automata ⋮ Büchi Automata Can Have Smaller Quotients ⋮ Organising LTL monitors over distributed systems with a global clock ⋮ Transformation from PLTL to automata via NFGs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Analog property checkers: a DDR2 case study ⋮ Incremental reasoning on monadic second-order logics with logic programming ⋮ A weakness measure for GR(1) formulae ⋮ Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking ⋮ GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic ⋮ State of Büchi Complementation ⋮ Mediating for reduction (on minimizing alternating Büchi automata) ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Advanced Ramsey-Based Büchi Automata Inclusion Testing ⋮ On the Relationship between LTL Normal Forms and Büchi Automata ⋮ SAT-based explicit LTL reasoning and its application to satisfiability checking ⋮ From complementation to certification ⋮ Qualitative analysis of gene regulatory networks by temporal logic
This page was built for publication:
