Real-time logics: Complexity and expressiveness
From MaRDI portal
Publication:689093
DOI10.1006/INCO.1993.1025zbMATH Open0791.68103OpenAlexW2139891885MaRDI QIDQ689093FDOQ689093
Rajeev Alur, Thomas A. Henzinger
Publication date: 6 December 1993
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/9e1e0038a991110610c4358a4e3dea84ab5fe736
Recommendations
verificationspecificationpropositional temporal logicreal-time temporal logicsreal-time temporal systemstimed state sequences
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cited In (83)
- Title not available (Why is that?)
- Optimal bounds in parametric LTL games
- Timed hyperproperties
- Title not available (Why is that?)
- Modular abstractions for verifying real-time distributed systems
- A Logical Characterisation of Event Clock Automata
- A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
- Metric temporal logic revisited
- Two-sorted metric temporal logics
- Reasoning about real-time repetitions: Terminating and nonterminating
- A contract-based approach to adaptivity
- The complexity of temporal logic over the reals
- Efficient timed model checking for discrete-time systems
- Verification from Declarative Specifications Using Logic Programming
- Adequacy and complete axiomatization for timed modal logic
- An automata-theoretic approach to constraint LTL
- Advances in Parametric Real-Time Reasoning
- LARS: a logic-based framework for analytic reasoning over streams
- Decidable metric logics
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Timeline-based planning over dense temporal domains
- Programming in metric temporal logic
- Solving multi-granularity temporal constraint networks
- Using mappings to prove timing properties
- A process algebra of communicating shared resources with dense time and priorities
- Compositional verification of real-time systems with explicit clock temporal logic
- Checking EMTLK properties of timed interpreted systems via bounded model checking
- Timer formulas and decidable metric temporal logic
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers
- Presburger liveness verification of discrete timed automata.
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
- A space-efficient on-the-fly algorithm for real-time model checking
- Planning control rules for reactive agents
- Invariant-driven specifications in Maude
- Theorem proving for pointwise metric temporal logic over the naturals via translations
- Timed CSP = closed timed automata
- Min-max Computation Tree Logic
- On the expressiveness of TPTL and MTL
- Proving properties of continuous systems: Qualitative simulation and temporal logic
- Time-Bounded Verification
- Robustness of temporal logic specifications for continuous-time signals
- HRELTL: a temporal logic for hybrid systems
- Model-checking Timed Temporal Logics
- Model Checking Real-Time Systems
- Title not available (Why is that?)
- The taming (timing) of the states
- Metric temporal reasoning with less than two clocks
- Time-budgeting: a component based development methodology for real-time embedded systems
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- Decidable integration graphs.
- Verification of reactive systems using temporal logic with clocks
- Decidability and Expressive Power of Real Time Logics
- Title not available (Why is that?)
- The expressive power of clocks
- Decidability results for metric and layered temporal logics
- Decidability and complexity of action-based temporal planning over dense time
- MTL with Bounded Variability: Decidability and Complexity
- Some Recent Results in Metric Temporal Logic
- Real-Time Definable Languages
- Completeness results for two-sorted metric temporal logics
- LTL over integer periodicity constraints
- Title not available (Why is that?)
- Min-max event-triggered computation tree logic
- Title not available (Why is that?)
- Can you answer while you wait?
- Context-free timed formalisms: robust automata and linear temporal logics
- Embedding online runtime verification for fault disambiguation on Robonaut2
- Parameterized model checking of weighted networks
- ``Most of leads to undecidability: failure of adding frequencies to LTL
- Title not available (Why is that?)
- Deciding FO-rewritability of Regular Languages and Ontology-Mediated Queries in Linear Temporal Logic
- One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
- From non-punctuality to non-adjacency: a quest for decidability of timed temporal logics with quantifiers
- Past is for free: on the complexity of verifying linear temporal properties with past
- Path Checking for MTL and TPTL over Data Words
- On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing
- Generalizing Non-punctuality for Timed Temporal Logic with Freeze Quantifiers
- SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
- Bounded variability of metric temporal logic
- A decidable timeout-based extension of linear temporal logic
- Making Metric Temporal Logic Rational
- A restricted second-order logic for non-deterministic poly-logarithmic time
This page was built for publication: Real-time logics: Complexity and expressiveness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q689093)
