Reasoning about infinite computations
From MaRDI portal
Publication:1341752
DOI10.1006/inco.1994.1092zbMath0827.03009DBLPjournals/iandc/VardiW94OpenAlexW1990609140WikidataQ55952477 ScholiaQ55952477MaRDI QIDQ1341752
Publication date: 13 December 1995
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: http://orbi.ulg.ac.be/handle/2268/116648
complexitydecision problemsexpressive powerPSPACE-completealternating automataprocess logicconnectives defined by finite automata on infinite wordsextensions of temporal logic
Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Modal logic (including the logic of norms) (03B45) Automata and formal grammars in connection with logical questions (03D05) Complexity of computation (including implicit computational complexity) (03D15)
Related Items (only showing first 100 items - show all)
Abstract interpretation as automated deduction ⋮ From LTL to deterministic automata. A safraless compositional approach ⋮ Model Checking Information Flow in Reactive Systems ⋮ Effective Synthesis of Asynchronous Systems from GR(1) Specifications ⋮ The complementation problem for Büchi automata with applications to temporal logic ⋮ Spanning the spectrum from safety to liveness ⋮ Quantitative solution of omega-regular games ⋮ Size-Change Termination and Satisfiability for Linear-Time Temporal Logics ⋮ The Complexity of Reversal-Bounded Model-Checking ⋮ Temporal Logic and Fair Discrete Systems ⋮ Verification of agent navigation in partially-known environments ⋮ GSTE is partitioned model checking ⋮ Weighted LTL with Discounting ⋮ When are stochastic transition systems tameable? ⋮ On decidability properties of local sentences ⋮ Tableau-based automata construction for dynamic linear time temporal logic ⋮ Logic programming approach to automata-based decision procedures ⋮ On the complexity of determinizing monitors ⋮ An automata-theoretic approach to constraint LTL ⋮ Bounded model checking of ETL cooperating with finite and looping automata connectives ⋮ Safraless LTL synthesis considering maximal realizability ⋮ Latticed-LTL synthesis in the presence of noisy inputs ⋮ Fuzzy alternating Büchi automata over distributive lattices ⋮ Branching-time logics with path relativisation ⋮ Automata-theoretic decision of timed games ⋮ Parameterized linear temporal logics meet costs: still not costlier than LTL ⋮ Model-Checking Linear-Time Properties of Quantum Systems ⋮ Parameterized Weighted Containment ⋮ Robust, expressive, and quantitative linear temporal logics: pick any two for free ⋮ Inherent Vacuity in Lattice Automata ⋮ Axiomatising extended computation tree logic ⋮ Unification of infinite sets of terms schematized by primal grammars ⋮ An interface theory for service-oriented design ⋮ A polynomial space construction of tree-like models for logics with local chains of modal connectives ⋮ On temporal logic versus Datalog ⋮ Coping with selfish on-going behaviors ⋮ Synthesizing Non-Vacuous Systems ⋮ Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects ⋮ Reasoning about sequences of memory states ⋮ Verification of gap-order constraint abstractions of counter systems ⋮ \textit{Once} and \textit{for all} ⋮ Optimized temporal monitors for SystemcC ⋮ Symbolic bounded synthesis ⋮ Linear temporal logic symbolic model checking ⋮ Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited ⋮ Finite-word hyperlanguages ⋮ Certifying inexpressibility ⋮ A complete characterization of deterministic regular liveness properties ⋮ On the Unusual Effectiveness of Logic in Computer Science ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ On relative and probabilistic finite counterability ⋮ Alternating-time temporal logics with linear past ⋮ Visibly linear temporal logic ⋮ Quantitative model-checking of controlled discrete-time Markov processes ⋮ Parametric linear dynamic logic ⋮ Infinite trees and automaton-definable relations over \(\omega\)-words ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ Infinite games with finite knowledge gaps ⋮ Transformation from PLTL to automata via NFGs ⋮ Probabilization of logics: completeness and decidability ⋮ Bridging the gap between fair simulation and trace inclusion ⋮ Alternating automata and temporal logic normal forms ⋮ \(\omega\)-regular languages are testable with a constant number of queries ⋮ Weak Muller acceptance conditions for tree automata ⋮ Reasoning about XML with temporal logics and automata ⋮ PSPACE-completeness of modular supervisory control problems ⋮ Strategy logic ⋮ Multi-robot LTL planning under uncertainty ⋮ LTL over integer periodicity constraints ⋮ CTL\(^\ast\) with graded path modalities ⋮ Distributed synthesis for parameterized temporal logics ⋮ Visibly linear dynamic logic ⋮ Model checking of linear-time properties in multi-valued systems ⋮ The alternation hierarchy in fixpoint logic with chop is strict too ⋮ Efficient model checking for LTL with partial order snapshots ⋮ Prime languages ⋮ Determinizing monitors for HML with recursion ⋮ A theory of monitors ⋮ Vacuity in synthesis ⋮ Classifying regular languages by a split game ⋮ Partitioned PLTL model-checking for refined transition systems ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ Before and after vacuity ⋮ \( \omega \)-automata ⋮ From liveness to promptness ⋮ Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past ⋮ Complexity and succinctness issues for linear-time hybrid logics ⋮ Dynamic linear time temporal logic ⋮ A verification-driven framework for iterative design of controllers ⋮ EXPtime tableaux for ALC ⋮ \(\mathsf{GR}(1)\) is equivalent to \(\mathsf{R}(1)\) ⋮ From complementation to certification ⋮ Relating word and tree automata ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL. ⋮ Verification by augmented finitary abstraction ⋮ Module checking ⋮ On the complexity of verifying concurrent transition systems ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Synthesis in presence of dynamic links ⋮ Qualitative analysis of gene regulatory networks by temporal logic
This page was built for publication: Reasoning about infinite computations
