Temporal logic can be more expressive
From MaRDI portal
Publication:3317085
DOI10.1016/S0019-9958(83)80051-5zbMath0534.03009OpenAlexW2806619258MaRDI QIDQ3317085
Publication date: 1983
Published in: Information and Control (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0019-9958(83)80051-5
modal logicregular expressionstemporal logicsatisfiabilitycomplexity of proofsdecision proceduretemporal operatorsright-linear grammars
Modal logic (including the logic of norms) (03B45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Complexity of proofs (03F20)
Related Items (only showing first 100 items - show all)
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints ⋮ Foundations of Boolean stream runtime verification ⋮ A derivation-loop method for temporal logic ⋮ A branching time logic with past operators ⋮ Cut-free sequent and tableau systems for propositional Diodorean modal logics ⋮ Bounded model checking of infinite state systems ⋮ A generalized time quantifier approach to approximate reasoning ⋮ The complementation problem for Büchi automata with applications to temporal logic ⋮ The computational complexity of scenario-based agent verification and design ⋮ Size-Change Termination and Satisfiability for Linear-Time Temporal Logics ⋮ Property preserving abstractions for the verification of concurrent systems ⋮ Temporal Logic and Fair Discrete Systems ⋮ Functional Specification of Hardware via Temporal Logic ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Incorporating monitors in reactive synthesis without paying the price ⋮ Complexity of modal logics with Presburger constraints ⋮ Recognizing safety and liveness ⋮ Interpreting message flow graphs ⋮ Tableau-based automata construction for dynamic linear time temporal logic ⋮ A mathematical framework for the semantics of symbolic languages representing periodic time ⋮ Invariant-free clausal temporal resolution ⋮ On the freeze quantifier in Constraint LTL: Decidability and complexity ⋮ An automata-theoretic approach to constraint LTL ⋮ Bounded model checking of ETL cooperating with finite and looping automata connectives ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ Parameterized linear temporal logics meet costs: still not costlier than LTL ⋮ A complete proof system for propositional projection temporal logic ⋮ Robust, expressive, and quantitative linear temporal logics: pick any two for free ⋮ Axiomatising extended computation tree logic ⋮ On projective and separable properties ⋮ Separation logics and modalities: a survey ⋮ One-Pass Tableaux for Computation Tree Logic ⋮ Knowledge forgetting in propositional \(\mu\)-calculus ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ Model checking of pushdown systems for projection temporal logic ⋮ Expressiveness of propositional projection temporal logic with star ⋮ Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects ⋮ \textit{Once} and \textit{for all} ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SnS can be modally characterized ⋮ Transformation of dynamic integrity constraints into transaction specifications ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mathematical modal logic: A view of its evolution ⋮ LTL is closed under topological closure ⋮ Linear temporal logic symbolic model checking ⋮ Specification of communicating processes: temporal logic versus refusals-based refinement ⋮ TABLEAUX: A general theorem prover for modal logics ⋮ Temporal logics with language parameters ⋮ On Gabbay's temporal fixed point operator ⋮ First-order rewritability of ontology-mediated queries in linear temporal logic ⋮ The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\) ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Visibly linear temporal logic ⋮ Parametric linear dynamic logic ⋮ A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata ⋮ Serializable histories in quantified propositional temporal logic ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ A decision procedure for propositional projection temporal logic with infinite models ⋮ The stuttering principle revisited ⋮ Bridging the gap between fair simulation and trace inclusion ⋮ Almost event-rate independent monitoring ⋮ CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks ⋮ Characterizing CTL-like logics on finite trees. ⋮ On regular temporal logics with past ⋮ From Philosophical to Industrial Logics ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ LTL over integer periodicity constraints ⋮ Cycle detection in computation tree logic ⋮ Distributed synthesis for parameterized temporal logics ⋮ Axiomatic semantics of projection temporal logic programs ⋮ Visibly linear dynamic logic ⋮ Regular \(\omega\)-languages with an informative right congruence ⋮ One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\) ⋮ Complexity of propositional projection temporal logic with star ⋮ Property-Based Testing for Spark Streaming ⋮ Reasoning about strings in databases ⋮ Temporal logic with recursion ⋮ Variable and clause elimination for LTL satisfiability checking ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ Expressive Completeness for LTL With Modulo Counting and Group Quantifiers ⋮ A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time ⋮ Egalitarian State-Transition Systems ⋮ An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ Sequences, datalog, and transducers ⋮ Dual systems of tableaux and sequents for PLTL ⋮ From complementation to certification ⋮ Temporal connectives versus explicit timestamps to query temporal databases ⋮ Expressive completeness of modal logic on binary ramified frames ⋮ 2005 Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '05 ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Process logic with regular formulas ⋮ On the expressive power of temporal logic for infinite words ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ A goal-directed decision procedure for hybrid PDL ⋮ Temporal logics of “the next” do not have the beth property ⋮ A theory of timed automata
This page was built for publication: Temporal logic can be more expressive
