The temporal semantics of concurrent programs

DOI10.1016/0304-3975(81)90110-9zbMath0441.68010OpenAlexW1970603830MaRDI QIDQ1143164

Publication date: 1981

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(81)90110-9

zbMATH Keywords

temporal logic semantics of concurrent programs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items (80)

Non-standard algorithmic and dynamic logic ⋮ A formalization of programs in first-order logic with a discrete linear order ⋮ Does “N+1 times” prove more programs correct than “N times”? ⋮ Compositionality of Hennessy-Milner logic by structural operational semantics ⋮ Church's Problem Revisited ⋮ A fixpoint theory for non-monotonic parallelism ⋮ The complementation problem for Büchi automata with applications to temporal logic ⋮ Automata-theoretic techniques for modal logics of programs ⋮ Ultraproducts and possible worlds semantics in institutions ⋮ A logic for reasoning about time and reliability ⋮ Model Checking of Biological Systems ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL ⋮ Checking interval properties of computations ⋮ Feature interaction detection by pairwise analysis of LTL properties -- A case study ⋮ Automata-driven partial order reduction and guided search for LTL model checking ⋮ Question-guided stubborn set methods for state properties ⋮ The power of temporal proofs ⋮ Concurrent systems and inevitability ⋮ Weak second order characterizations of various program verification systems ⋮ A semantics for concurrent separation logic ⋮ Resources, concurrency, and local reasoning ⋮ Reasoning about time in the situation calculus ⋮ Assumption/guarantee specifications in linear-time temporal logic (extended abstract) ⋮ Taming strategy logic: non-recurrent fragments ⋮ Fuzzy Halpern and Shoham's interval temporal logics ⋮ Action and State Based Computation Tree Measurement Language and Algorithms ⋮ A simple rewrite system for the normalization of linear temporal logic ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ Reasoning About Substructures and Games ⋮ Model checking of pushdown systems for projection temporal logic ⋮ The language of social software ⋮ Unnamed Item ⋮ Distributed breadth-first search LTL model checking ⋮ Reliability-aware automatic composition approach for web services ⋮ Parallel algorithms for the single source shortest path problem ⋮ Unnamed Item ⋮ Mathematical modal logic: A view of its evolution ⋮ On the computational complexity of behavioral description-based web service composition ⋮ Appraising two decades of distributed computing theory research ⋮ Specification of communicating processes: temporal logic versus refusals-based refinement ⋮ Bounded semantics ⋮ Compositionality and bisimulation: A negative result ⋮ Assumption/guarantee specifications in linear-time temporal logic ⋮ On relative and probabilistic finite counterability ⋮ Embedding finite automata within regular expressions ⋮ Unnamed Item ⋮ Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations ⋮ Query-based verification of qualitative trends and oscillations in biochemical systems ⋮ Alternative semantics for temporal logics ⋮ A modular approach to defining and characterising notions of simulation ⋮ Test generation from P systems using model checking ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Temporal logic programming ⋮ ‘What I Fail to Do Today, I Have to Do Tomorrow’: A Logical Study of the Propagation of Obligations ⋮ Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy ⋮ Converting a Büchi alternating automaton to a usual nondeterministic one ⋮ Model Checking LTL Formulae in RAISE with FDR ⋮ Prime languages ⋮ Computation tree measurement language (CTML) ⋮ Branching-Time Temporal Logics with Minimal Model Quantifiers ⋮ Extended Stochastic Petri Nets for Model-Based Design of Wetlab Experiments ⋮ Decision Procedures for a Deontic Logic Modeling Temporal Inheritance of Obligations ⋮ Game-theoretic simulation checking tool ⋮ Is ``Some-other-time sometimes better than ``Sometime for proving partial correctness of programs? ⋮ Deductive verification of simple foraging robotic behaviours ⋮ Calculi for synchrony and asynchrony ⋮ The temporal logic of branching time ⋮ Model-Based Testing for Functional and Security Test Generation ⋮ An approach to automating the verification of compact parallel coordination programs. I ⋮ Ten years of Hoare's logic: A survey. II: Nondeterminism ⋮ A generalized nexttime operator in temporal logic ⋮ Syntax-directed model checking of sequential programs ⋮ Synthesis in presence of dynamic links ⋮ Compositional verification of asynchronous concurrent systems using CADP ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq ⋮ Timed network games ⋮ Good-for-Game QPTL: An Alternating Hodges Semantics ⋮ Checking timed Büchi automata emptiness efficiently ⋮ Back to the future: a fresh look at linear temporal logic

Cites Work

This page was built for publication: The temporal semantics of concurrent programs