An Automata-Theoretic Approach to Linear Temporal Logic

No abstract is available for this paper.

• Publication year

  1996

• Venue

  Banff Higher Order Workshop

• Publication date

  1996-04-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-60915-6_6
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Descriptive Set Theory

  1997cited by this paper
• Introduction to algorithms

  1996cited by this paper
• Reasoning About Infinite Computations

  1994cited by this paper
• Nontraditional Applications of Automata Theory

  1994cited by this paper
• The Temporal Logic of Reactive and Concurrent Systems

  1991cited by this paper
• Automata on Infinite Objects

  1991cited by this paper
• Memory-efficient algorithms for the verification of temporal properties

  1990cited by this paper
• On the Development of Reactive Systems

  1989cited by this paper
• Realizable and Unrealizable Specifications of Reactive Systems

  1989cited by this paper
• On the synthesis of a reactive module

  1989cited by this paper
• On simultaneously determinizing and complementing omega -automata

  1989cited by this paper
• Trace theory for automatic hierarchical verification of speed-independent circuits

  1989cited by this paper
• The complexity of tree automata and logics of programs

  1988cited by this paper
• Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time

  1988cited by this paper
• On the complexity of omega -automata

  1988cited by this paper
• Modalities for Model Checking: Branching Time Logic Strikes Back

  1987cited by this paper
• Temporal Logic of Programs

  1987cited by this paper
• Alternating Automata on Infinite Trees

  1987cited by this paper
• Network Protocols and Tools to Help Produce Them

  1987cited by this paper
• The Complementation Problem for Büchi Automata with Appplications to Temporal Logic

  1987cited by this paper
• Alternating automata on infinite trees

  1987cited by this paper
• An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

  1986cited by this paper
• “Sometimes” and “not never” revisited: on branching versus linear time temporal logic

  1986cited by this paper
• The complexity of propositional linear temporal logics

  1985cited by this paper
• Checking that finite state concurrent programs satisfy their linear specification

  1985cited by this paper
• Automata, Tableaux and Temporal Logics (Extended Abstract)

  1985cited by this paper
• The Glory of the Past

  1985cited by this paper
• Modalities for model checking (extended abstract): branching time strikes back

  1985cited by this paper
• Improved upper and lower bounds for modal logics of programs

  1985cited by this paper
• Model Checking Under Generalized Fairness Constraints

  1984cited by this paper
• Sometimes and Not Never Revisited: on Branching Versus Linear Time

  1984cited by this paper
• Alternating Finite Automata on omega-Words

  1984cited by this paper
• Reasoning about infinite computation paths

  1983cited by this paper
• Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons

  1982cited by this paper
• The NP-Completeness Column: An Ongoing Guide

  1982cited by this paper
• The complexity of propositional linear temporal logics

  1982cited by this paper
• Is the interesting part of process logic uninteresting?: a translation from PL to PDL

  1982cited by this paper
• Using Branching Time Logic to Synthesize Synchronization Skeletons

  1982cited by this paper
• Proving Liveness Properties of Concurrent Programs

  1982cited by this paper
• Succint Representation of Regular Languages by Boolean Automata

  1981cited by this paper
• Synthesis of Communicating Processes from Temporal Logic Specifications

  1981cited by this paper
• On the temporal analysis of fairness

  1980cited by this paper
• "Sometime" is sometimes "not never": on the temporal logic of programs

  1980cited by this paper
• On Equations for Regular Languages, Finite Automata, and Sequential Networks

  1980cited by this paper
• Introduction to Automata Theory, Languages and Computation

  1979cited by this paper
• Johnson: computers and intractability: a guide to the theory of np- completeness (freeman

  1979cited by this paper
• Space-Bounded Reducibility among Combinatorial Problems

  1975cited by this paper
• Theories of Automata on omega-Tapes: A Simplified Approach

  1974cited by this paper
• The Emptiness Problem for Automata on Infinite Trees

  1972cited by this paper
• Automata on Infinite Objects and Church's Problem

  1972cited by this paper
• The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Space

  1972cited by this paper
• Economy of Description by Automata, Grammars, and Formal Systems

  1971cited by this paper
• Relationships Between Nondeterministic and Deterministic Tape Complexities

  1970cited by this paper
• Solving sequential conditions by finite-state strategies

  1969cited by this paper
• Decidability of second-order theories and automata on infinite trees

  1968cited by this paper
• Testing and Generating Infinite Sequences by a Finite Automaton

  1966cited by this paper
• 7. Infinite Games of Perfect Information

  1964cited by this paper
• Journal of the Association for Computing Machinery

  1961cited by this paper
• On a decision method in restricted second-order arithmetic

  1960cited by this paper
• Finite Automata and Their Decision Problems

  1959cited by this paper

• Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings

  2026cites this paper
• An Automata-Based Approach to Games with $\omega$-Automatic Preferences

  2026cites this paper
• MightyPPL: Verification of MITL with Past and Pnueli Modalities

  2025cites this paper
• Ensuring Reliability in Self-Adaptive Systems: A Framework for Formal Specification and Verification

  2025cites this paper
• LATMOS: Latent Automaton Task Model from Observation Sequences

  2025cites this paper
• Repairing Neural Network-based Control Policies with Safety Preservation

  2025cites this paper
• Formal verification of a machine learning tool for runway configuration assistance

  2025cites this paper
• Interpolation-Inspired Closure Certificates

  2025influential citation
• Automatic Generation of Safety-compliant Linear Temporal Logic via Large Language Model: A Self-supervised Framework

  2025cites this paper
• A Reinforcement Learning Algorithm for Safety Decision Making in Autonomous Driving Systems with Reward Machine Guidance

  2025cites this paper
• Defining neurosymbolic AI

  2025cites this paper
• Supporting Software Formal Verification with Large Language Models: An Experimental Study

  2025cites this paper
• Resolving Availability and Run-time Integrity Conflicts in Real-Time Embedded Systems

  2025cites this paper
• Analysing Temporal Reasoning in Description Logics Using Formal Grammars

  2025cites this paper
• AS2FM: Enabling Statistical Model Checking of ROS 2 Systems for Robust Autonomy

  2025cites this paper
• Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata

  2025influential citation
• Control Closure Certificates

  2025cites this paper
• Policy Gradient Methods for Information-Theoretic Opacity in Markov Decision Processes

  2025cites this paper
• A Variety of Request-Response Specifications

  2025cites this paper
• A Note on Runtime Verification of Concurrent Systems

  2025cites this paper
• Symbolic Automata: Omega-Regularity Modulo Theories

  2025cites this paper
• Neural Closure Certificates

  2024cites this paper
• Obstruction Alternating-time Temporal Logic: A Strategic Logic to Reason about Dynamic Models

  2024cites this paper
• Regular decision processes

  2024cites this paper
• Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs

  2024cites this paper
• Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis

  2024cites this paper
• Checking Complex Source Code-Level Constraints using Runtime Verification

  2024cites this paper
• Implicit Rankings for Verifying Liveness Properties in First-Order Logic

  2024cites this paper
• Temporal Ensemble Logic

  2024cites this paper
• Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges

  2024cites this paper
• SPEcBCFuzz: Fuzzing LTL Solvers with Boundary Conditions

  2024cites this paper
• Verifiably Following Complex Robot Instructions with Foundation Models

  2024cites this paper
• Verification of Hyperproperties for Dynamical Systems via Barrier Certificates

  2024cites this paper
• A formal model-based approach to design failure-aware Internet of Things architectures

  2024cites this paper
• Fuzzy Linear Temporal Logic with Quality Constraints

  2024cites this paper
• Antichain with SAT and Tries

  2024cites this paper
• Program Dependence Net Reduction for LTL Model Checking

  2024cites this paper
• Probabilistic Synthesis and Verification for LTL on Finite Traces

  2024influential citation
• Reach-Avoid Control Synthesis for a Quadrotor UAV with Formal Safety Guarantees

  2024cites this paper
• Lang2LTL-2: Grounding Spatiotemporal Navigation Commands Using Large Language and Vision-Language Models

  2024cites this paper
• Skill Transfer for Temporal Task Specification

  2024cites this paper
• MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm

  2024cites this paper
• Reactive Symbolic Planning and Control in Dynamic Adversarial Environments

  2023cites this paper
• EnPAC: Petri Net Model Checking for Linear Temporal Logic

  2023cites this paper
• Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments

  2023cites this paper
• Semantic Traffic Law Adaptive Decision-Making for Self-Driving Vehicles

  2023cites this paper
• Model consistency as a heuristic for eventual correctness

  2023cites this paper
• Formulas Expressing Totally Nonstable Truth Values of Formulas

  2023cites this paper
• Planning with Propositional Temporally Extended Goals Using Heuristic Search

  2023cites this paper
• Model-checking in the Foundations of Algorithmic Law and the Case of Regulation 561

  2023cites this paper
• Closure Certificates

  2023cites this paper
• Experiments on Infinite Model Finding in SMT Solving

  2023cites this paper
• Optimal Alignment of Temporal Knowledge Bases (Extended Abstract)

  2023cites this paper
• Learning Linear Temporal Properties for Autonomous Robotic Systems

  2023cites this paper
• Automated Formation Control Synthesis from Temporal Logic Specifications

  2023cites this paper
• Fulfilling Formal Specifications ASAP by Model-free Reinforcement Learning

  2023cites this paper
• On the Comparison of Discounted-Sum Automata with Multiple Discount Factors

  2023cites this paper
• Sports Injury Prediction in Professional Tennis

  2023cites this paper
• Reactive Synthesis of Dominant Strategies

  2023cites this paper
• Algorithms for recognizing formulas with none-stable truth values in branching time logic

  2023cites this paper
• Finite-Horizon Shield for Path Planning Ensuring Safety/Co-Safety Specifications and Security Policies

  2023cites this paper
• Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way

  2023cites this paper
• Symbolic Automata: ω-Regularity Modulo Theories

  2023influential citation
• Parameterized Model-checking of Discrete-Timed Networks and Symmetric-Broadcast Systems

  2023cites this paper
• Efficient Normalization of Linear Temporal Logic

  2023influential citation
• Probabilistic Black-Box Checking via Active MDP Learning

  2023cites this paper
• Prioritized Time-Point-Interval Petri Nets Modeling Multiprocessor Real-Time Systems and TCTL$_{x}$

  2023cites this paper
• An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification

  2023cites this paper
• Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

  2023influential citation
• Formal Modeling and Verification of Industrial Robotic Arm - A Case Study

  2023cites this paper
• Computing All Facts Entailed By An LTL Specification

  2023cites this paper
• Realizable and Context-Free Hyperlanguages

  2022cites this paper
• Reward Learning using Structural Motifs in Inverse Reinforcement Learning

  2022cites this paper
• Formal Verification of Safety Properties Using Interpolation and k-induction

  2022cites this paper
• Discrete Time Series Clustering and Delineation: A Tree-Based Approach to Linear Temporal Logic Discovery

  2022cites this paper
• On the Separation of Conditional XPath

  2022cites this paper
• Temporal Multi-Agents' Logics Modelling Dynamic Temporal Accessibility Relations

  2022cites this paper
• LTL-Transfer: Skill Transfer for Temporal Task Specification

  2022cites this paper
• Manipulation Task Planning and Motion Control Using Task Relaxations

  2022cites this paper
• Practical Applications of the Alternating Cycle Decomposition

  2022influential citation
• Statistical Model Checking for Probabilistic Temporal Epistemic Logics

  2022cites this paper
• starMC: an automata based CTL* model checker

  2022cites this paper
• Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata

  2022cites this paper
• Constructing Concise Characteristic Samples for Acceptors of Omega Regular Languages

  2022cites this paper
• Formal verification confirms the role of p53 protein in cell fate decision mechanism

  2022influential citation
• Verification modulo theories

  2022cites this paper
• Little Tricky Logic: Misconceptions in the Understanding of LTL

  2022cites this paper
• Lost in Translation: from Linear Temporal Logic to Büchi Automata

  2022influential citation
• Structural Coverage of LTL Requirements for Learning-based Testing

  2022cites this paper
• Verification and Realizability in Finite-Horizon Multiagent Systems

  2022influential citation
• Ain’t No Stopping Us Monitoring Now

  2022cites this paper
• Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

  2021cites this paper
• Formal Verification for Autopilot – Preliminary state of the Art

  2021cites this paper
• Sampling Polynomial Trajectories for LTL Verification

  2021cites this paper
• Compositional Approach to Translate LTLf/LDLf into Deterministic Finite Automata

  2021influential citation
• Supervised Bayesian specification inference from demonstrations

  2021cites this paper
• City, University of London Institutional Repository City Research Online

  2021cites this paper
• From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle

  2021cites this paper
• Verifying Computation Tree Logic of Knowledge via Knowledge-Oriented Petri Nets and Ordered Binary Decision Diagrams

  2021cites this paper
• Disturbance Bounds for Signal Temporal Logic Task Satisfaction: A Dynamics Perspective

  2021cites this paper