scientific article; zbMATH DE number 2102710
From MaRDI portal
zbMath1046.68588MaRDI QIDQ4817549
Moshe Y. Vardi, Marco Daniele, Fausto Giunchiglia
Publication date: 24 September 2004
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items
From LTL to deterministic automata. A safraless compositional approach, A Logical Approach to Data-Aware Automated Sequence Generation, A symbolic decision procedure for symbolic alternating finite automata, An abstraction-refinement methodology for reasoning about network games, Model Checking Probabilistic Systems, Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL, GSTE is partitioned model checking, Tableau-based automata construction for dynamic linear time temporal logic, Logic programming approach to automata-based decision procedures, Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition, From linear temporal logics to Büchi automata: the early and simple principle, Bridging the gap between single- and multi-model predictive runtime verification, The effects of semantic simplifications on random \textit{BST}-like expression-trees, Towards a notion of unsatisfiable and unrealizable cores for LTL, An explicit transition system construction approach to LTL satisfiability checking, Optimized temporal monitors for SystemcC, Linear temporal logic symbolic model checking, Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations \textit{Until} and \textit{Since} based on bundles of integer numbers, logical consecutions, deciding algorithms, Büchi Store: An Open Repository of Büchi Automata, Linear temporal logic with until and next, logical consecutions, Inference Rules in Multi-agents’ Temporal Logics, Transformation from PLTL to automata via NFGs, Reasoning about XML with temporal logics and automata, Incremental reasoning on monadic second-order logics with logic programming, Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking, GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic, Tool support for learning Büchi automata and linear temporal logic, On the Relationship between LTL Normal Forms and Büchi Automata, SAT-based explicit LTL reasoning and its application to satisfiability checking, More efficient on-the-fly LTL verification with Tarjan's algorithm
Uses Software
