Reasoning about infinite computations

DOI10.1006/inco.1994.1092zbMath0827.03009OpenAlexW1990609140WikidataQ55952477 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

zbMATH Keywords

complexity decision problems expressive power PSPACE-complete alternating automata process logic connectives defined by finite automata on infinite words extensions of temporal logic

Mathematics Subject Classification ID

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

The Hybrid Plan Controller Construction for Trajectories in Sobolev Space, Ramsey-Based Inclusion Checking for Visibly Pushdown Automata, On Composing Finite Forests with Modal Logics, Automata Theory and Model Checking, Explicit-State Model Checking, SAT-Based Model Checking, Graph Games and Reactive Synthesis, Model Checking Probabilistic Systems, Symbolic Model Checking in Non-Boolean Domains, Multi-Valued Reasoning about Reactive Systems, Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL, Temporal equilibrium logic: a survey, Expressiveness and succinctness of a logic of robustness, A CTL* Model Checker for Petri Nets, Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis, Zielonka DAG acceptance and regular languages over infinite words, \textsc{Pspace}-completeness of the temporal logic of sub-intervals and suffixes, Linear-Time Model Checking: Automata Theory in Practice, LTL model checking of self modifying code, Specifiable robustness in reactive synthesis, HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems, Temporal stream logic modulo theories, A space-efficient on-the-fly algorithm for real-time model checking, An algorithmic approach for checking closure properties of Ω-regular languages, Tableaux for realizability of safety specifications, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Mapping Properties of Heterogeneous Ontologies, Unnamed Item, Knowledge-based programs, Axiomatising extended computation tree logic, Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations, On the complexity of verifying concurrent transition systems, The Quest for a Tight Translation of Büchi to co-Büchi Automata, An Automata-Theoretic Approach to Infinite-State Systems, An Automata-based Approach for CTL⋆ With Constraints, Unnamed Item, Verification by augmented abstraction: The automata-theoretic view, On the complexity of resource-bounded logics, Finite-word hyperlanguages, From Philosophical to Industrial Logics, From Monadic Logic to PSL, Incremental reasoning on monadic second-order logics with logic programming, Automata-Theoretic Model Checking Revisited, Lattice Automata, Better Under-Approximation of Programs by Hiding Variables, Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata, On Omega-Languages Defined by Mean-Payoff Conditions, Synthesis from Component Libraries, Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking, Model Checking-Based Genetic Programming with an Application to Mutual Exclusion, On Verifying Fault Tolerance of Distributed Protocols, The Complexity of CTL* + Linear Past, Random Models for Evaluating Efficient Büchi Universality Checking, On Repetition Languages, Description Logics, Minimizing GFG Transition-Based Automata, Unnamed Item, BÜCHI COMPLEMENTATION MADE TIGHTER, TYPENESS FOR ω-REGULAR AUTOMATA, Linear-time temporal logics with Presburger constraints: an overview ★, Alternating automata: Unifying truth and validity checking for temporal logics, Runtime Verification Using a Temporal Description Logic, Consistently-detecting monitors, REASONING ABOUT TRANSFINITE SEQUENCES, Backward Deterministic Büchi Automata on Infinite Words, How Deterministic are Good-For-Games Automata?, 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