Real-time logics: Complexity and expressiveness

DOI10.1006/inco.1993.1025zbMath0791.68103OpenAlexW2139891885MaRDI QIDQ689093

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

zbMATH Keywords

verification specification propositional temporal logic real-time temporal logics real-time temporal systems timed state sequences

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Metric temporal logic revisited, Solving multi-granularity temporal constraint networks, Presburger liveness verification of discrete timed automata., Timed hyperproperties, Decidability and complexity of action-based temporal planning over dense time, Adequacy and complete axiomatization for timed modal logic, Efficient timed model checking for discrete-time systems, Invariant-driven specifications in Maude, Metric temporal reasoning with less than two clocks, Time-Bounded Verification of CTMCs against Real-Time Specifications, Path Checking for MTL and TPTL over Data Words, Model Checking Real-Time Systems, Checking EMTLK properties of timed interpreted systems via bounded model checking, Time-Bounded Verification, LARS: a logic-based framework for analytic reasoning over streams, An automata-theoretic approach to constraint LTL, Compositional verification of real-time systems with explicit clock temporal logic, Bounded variability of metric temporal logic, Programming in metric temporal logic, A decidable timeout-based extension of linear temporal logic, SMT-based satisfiability of first-order LTL with event freezing functions and metric operators, Optimal bounds in parametric LTL games, Completeness results for two-sorted metric temporal logics, Planning control rules for reactive agents, A process algebra of communicating shared resources with dense time and priorities, Two-sorted metric temporal logics, HRELTL: a temporal logic for hybrid systems, Pushdown timed automata: A binary reachability characterization and safety verification., Deciding FO-rewritability of Regular Languages and Ontology-Mediated Queries in Linear Temporal Logic, Proving properties of continuous systems: Qualitative simulation and temporal logic, A space-efficient on-the-fly algorithm for real-time model checking, The complexity of temporal logic over the reals, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Parameterized model checking of weighted networks, Some Recent Results in Metric Temporal Logic, MTL with Bounded Variability: Decidability and Complexity, A Logical Characterisation of Event Clock Automata, Theorem proving for pointwise metric temporal logic over the naturals via translations, ``Most of leads to undecidability: failure of adding frequencies to LTL, The expressive power of clocks, Timeline-based planning over dense temporal domains, Modular abstractions for verifying real-time distributed systems, Embedding online runtime verification for fault disambiguation on Robonaut2, Using mappings to prove timing properties, A temporal logic for micro- and macro-step-based real-time systems: foundations and applications, A contract-based approach to adaptivity, Min-max Computation Tree Logic, On the expressiveness of TPTL and MTL, Timer formulas and decidable metric temporal logic, LTL over integer periodicity constraints, One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\), Decidable metric logics, Robustness of temporal logic specifications for continuous-time signals, Time-budgeting: a component based development methodology for real-time embedded systems, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing, Decidability results for metric and layered temporal logics, Model-checking Timed Temporal Logics, Verification of reactive systems using temporal logic with clocks, Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past, Timed CSP = Closed Timed Automata1, Making Metric Temporal Logic Rational, Verification from Declarative Specifications Using Logic Programming, Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers, Min-max event-triggered computation tree logic, Decidable integration graphs., Can you answer while you wait?, Is your model checker on time? On the complexity of model checking for timed modal logics, Context-free timed formalisms: robust automata and linear temporal logics