Model Checking Quantitative Linear Time Logic

DOI10.1016/J.ENTCS.2008.11.019MaRDI QIDQ5415664zbMATHOpenAlexFDO

Authors Marco Faella, Axel Legay, Mariëlle I. A. Stoelinga

Publication date 13 May 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.11.019

zbMATH Keywords

automatalinear temporal logicquantitative verification

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites work

• scientific article; zbMATH DE number 2038772 (Why is no real title available?)
• scientific article; zbMATH DE number 1744958 (Why is no real title available?)
• scientific article; zbMATH DE number 1754609 (Why is no real title available?)
• scientific article; zbMATH DE number 1786477 (Why is no real title available?)
• A logic for reasoning about time and reliability
• A theory of timed automata
• An automata-theoretic approach to branching-time model checking
• An optimal automata approach to LTL model checking of probabilistic systems
• Automata, Languages and Programming
• Model Checking Software
• Model checking discounted temporal properties
• Model checking of probabilistic and nondeterministic systems
• Testing and generating infinite sequences by a finite automaton
• The Büchi Complementation Saga
• The complexity of probabilistic verification
• Validation of Stochastic Systems

Cited in

(11)

• On the complexity of verification of time-sensitive distributed systems
• Weighted LTL with discounting
• Parity Automata for Quantitative Linear Time Logics
• Synthesis from component libraries with costs
• On high-quality synthesis
• Linear-time logics -- a coalgebraic perspective
• Latticed-LTL synthesis in the presence of noisy inputs
• Model Checking Quantified Computation Tree Logic
• Symbolic model checking in non-Boolean domains
• Multi-Valued Reasoning about Reactive Systems
• Quantitative vs. weighted automata

Describes a project that uses

Uses Software

• LiQuor

This page was built for publication: Model Checking Quantitative Linear Time Logic

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