A really temporal logic

DOI10.1145/174644.174651zbMath0807.68065OpenAlexW2030263557WikidataQ56092495 ScholiaQ56092495MaRDI QIDQ4299300

Thomas A. Henzinger, Rajeev Alur

Publication date: 8 March 1995

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/174644.174651

zbMATH Keywords

real-time systemstemporal logictableau-based decision procedurefreeze quantifiermodel-checking algorithm

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Temporal Minimal-World Query Answering over Sparse ABoxes, Satisfiability of quantitative probabilistic CTL: rise to the challenge, Linear Time Monitoring for One Variable TPTL, A space-efficient on-the-fly algorithm for real-time model checking, The quest for an adequate semantic basis of dense-time metric temporal logic, Realizability problem for constraint LTL, Temporal Logic with Recursion., Metric temporal logic revisited, 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, The decision problem of modal product logics with a diagonal, and faulty counter machines, Model-checking CTL* over flat Presburger counter systems, Metric temporal reasoning with less than two clocks, On interactive knowledge with bounded communication, Time-Bounded Verification of CTMCs against Real-Time Specifications, The Complexity of Reversal-Bounded Model-Checking, Path Checking for MTL and TPTL over Data Words, Model Checking Real-Time Systems, The power of the ``always operator in first-order temporal logic, Model Checking of Biological Systems, Temporal Logic for Programmable Logic Controllers, Complexity of modal logics with Presburger constraints, On clock-aware LTL parameter synthesis of timed automata, On the freeze quantifier in Constraint LTL: Decidability and complexity, Axiomatisation and decidability of multi-dimensional Duration Calculus, Quantitative temporal logics over the reals: PSpace and below, An automata-theoretic approach to constraint LTL, Unnamed Item, Verifying a signature architecture: a comparative case study, Bounded variability of metric temporal logic, Programming in metric temporal logic, A decidable timeout-based extension of linear temporal logic, Temporal Specifications with Accumulative Values, A temporal logic for real-time partial-ordering with named transactions, A process algebra of communicating shared resources with dense time and priorities, A survey on temporal logics for specifying and verifying real-time systems, Deciding safety and liveness in TPTL, Undecidable Propositional Bimodal Logics and One-Variable First-Order Linear Temporal Logics with Counting, An SMT-based approach to satisfiability checking of MITL, Verification in loosely synchronous queue-connected discrete timed automata., Generalized discrete timed automata: Decidable approximations for safety verification., On the expressivity and complexity of quantitative branching-time temporal logics, Pushdown timed automata: A binary reachability characterization and safety verification., Reasoning about sequences of memory states, Completeness and decidability of tense logics closely related to logics above K4, Unnamed Item, Unnamed Item, Past pushdown timed automata and safety verification., Parameterized model checking of weighted networks, Quantifying conformance using the Skorokhod metric, Unnamed Item, Constraint LTL satisfiability checking without automata, Some Recent Results in Metric Temporal Logic, STL*: extending signal temporal logic with signal-value freezing operator, Theorem proving for pointwise metric temporal logic over the naturals via translations, Model Checking Biological Oscillators, Automatic synthesis of real time systems, A logic for metric and topology, Modular abstractions for verifying real-time distributed systems, Minimum and maximum delay problems in real-time systems, Modelling temporal behaviour in complex systems with Timebands, VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES, THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS, Semantics of temporal constrained objects, Verification of qualitative \(\mathbb Z\) constraints, A temporal logic for micro- and macro-step-based real-time systems: foundations and applications, A contract-based approach to adaptivity, Detecting synchronisation of biological oscillators by model checking, Monotonic hybrid systems, An interval-based temporal algebra based on binary encoding of point relations, Timed modal logics for real-time systems. Specification, verification and control, Linear reachability problems and minimal solutions to linear Diophantine equation systems, Min-max Computation Tree Logic, Ensuring completeness of symbolic verification methods for infinite-state systems, On the expressiveness of TPTL and MTL, Unnamed Item, Model checking restricted sets of timed paths, LTL over integer periodicity constraints, A real-time interval logic and its decision procedure, Completeness Results for Memory Logics, One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\), Monitoring Metric First-Order Temporal Properties, A logical characterization of timed regular languages, What good are digital clocks?, Property-Based Testing for Spark Streaming, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, Unnamed Item, On Freeze LTL with Ordered Attributes, Temporal logic with recursion, On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality, and Deterministic Freezing, Unnamed Item, Model-checking Timed Temporal Logics, Complexity issues for timeline-based planning over dense time under future and minimal semantics, Linear-time temporal logics with Presburger constraints: an overview ★, Realizability of Real-Time Logics, On a class of timer hybrid systems reducible to finite state automata, ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS, Min-max event-triggered computation tree logic, Decidable first-order transition logics for PA-processes, Model checking of systems with many identical timed processes, Is your model checker on time? On the complexity of model checking for timed modal logics, Satisfiability checking for mission-time \textsf{LTL} (MLTL), A fuzzy real-time temporal logic