scientific article

zbMath0607.68022MaRDI QIDQ3746875

Amir Pnueli

Publication date: 1986

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

surveyverificationtemporal logicreactive systemsproof systemmodular specificationfair transition system

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items (38)

Specification and verification of database dynamics ⋮ Property preserving abstractions for the verification of concurrent systems ⋮ Practical verification of multi-agent systems against \textsc{Slk} specifications ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ A temporal logic-based approach for the description of object behavior evolution ⋮ Fairness and the axioms of control predicates ⋮ Resolution-based approach to compatibility analysis of interacting automata ⋮ Programming in metric temporal logic ⋮ A theory of implementation and refinement in timed Petri nets ⋮ A first step towards implementing dynamic algebraic dependences ⋮ LTL-specification for development and verification of control programs ⋮ Event fairness and non-interleaving concurrency ⋮ On the interpretability of arithmetic in temporal logic ⋮ Safety and liveness from a methodological point of view ⋮ Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems ⋮ Symbolic checking of fuzzy CTL on fuzzy program graph ⋮ Functional specification and proof of correctness for time dependent behaviour of reactive systems ⋮ Completing the temporal picture ⋮ On agent-based software engineering ⋮ Operational specification with joint actions: Serializable databases ⋮ Defining conditional independence using collapses ⋮ Modeling and visualizing object-oriented programs with Codecharts ⋮ Sooner is safer than later ⋮ Verification of distributed programs using representative interleaving sequences ⋮ Capacitated automata and systems ⋮ An Incremental and Modular Technique for Checking LTL∖X Properties of Petri Nets ⋮ Robustness of temporal logic specifications for continuous-time signals ⋮ Prime languages ⋮ Property-Based Testing for Spark Streaming ⋮ Priority as extremal probability ⋮ An axiomatization of PCTL* ⋮ A probabilistic dynamic logic ⋮ Decidable fragments of first-order temporal logics ⋮ A multiprocess network logic with temporal and spatial modalities ⋮ Testing preorders for probabilistic processes. ⋮ Parameterised verification for multi-agent systems ⋮ A theory of timed automata

This page was built for publication: