The ForSpec temporal logic: A new temporal property-specification language

DOI10.1007/3-540-46002-0_21MaRDI QIDQ4472249zbMATH OpenFDO

Authors Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, A. Tiemeyer, Moshe Y. Vardi, Yael Zbar

Publication date 4 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2280/22800296.htm

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The temporal logic Sugar
• On Regular Temporal Logics with Past,
• A really temporal logic
• On regular temporal logics with past
• scientific article; zbMATH DE number 3889506

Cited in

(28)

• Distributed synthesis for parameterized temporal logics
• Incorporating monitors in reactive synthesis without paying the price
• An abstraction-refinement framework for trigger querying
• Compositional verification of asynchronous concurrent systems using CADP
• Automata theory and model checking
• Functional specification of hardware via temporal logic
• Linear-time temporal logic with event freezing functions
• Linear-Time Model Checking: Automata Theory in Practice
• Branching vs. Linear Time: Semantical Perspective
• From Philosophical to Industrial Logics
• Matching Trace Patterns with Regular Policies
• Bounded model checking of ETL cooperating with finite and looping automata connectives
• The definition of a temporal clock operator
• The temporal logic Sugar
• On temporal logic and signal processing
• Linear temporal logic symbolic model checking
• Runtime verification of embedded real-time systems
• Distributed PROMPT-LTL synthesis
• Propositional Dynamic Logic for Hyperproperties
• Parametric linear dynamic logic
• Safety and Liveness, Weakness and Strength, and the Underlying Topological Relations
• From Monadic Logic to PSL
• Automata-Theoretic Model Checking Revisited
• CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
• Temporal logics with language parameters
• Visibly linear temporal logic
• The use of contract specifications for representing requirements and for functional testing of hardware models
• On regular temporal logics with past

Describes a project that uses

Uses Software

• NuSMV

This page was built for publication: The ForSpec temporal logic: A new temporal property-specification language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4472249)