Model checking and synthesis for branching multi-weighted logics

DOI10.1016/J.JLAMP.2019.02.001MaRDI QIDQ2423760zbMATH OpenOpenAlexFDO

Authors Jiří Srba, Lasse S. Jensen, Isabella Kaufmann, Kim G. Larsen, Søren M. Nielsen

Publication date 20 June 2019

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2019.02.001

zbMATH Keywords

synthesismodel checkingtemporal logicsdependency graphsquantitative

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Synthesis for multi-weighted games with branching-time winning conditions
• Synthesis from LTL specifications with mean-payoff objectives
• Quantitative Verification of Weighted Kripke Structures
• Model checking for a class of weighted automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 5595162 (Why is no real title available?)
• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• A Deductive Approach to Program Synthesis
• Alternation-free weighted mu-calculus: decidability and completeness
• Energy games in multiweighted automata
• Extended dependency graphs and efficient distributed fixed-point computation
• Fixed-dimensional energy games are in pseudo-polynomial time
• Formally reasoning about quality
• Infinite Runs in Weighted Timed Automata with Energy Constraints
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• On the expressivity and complexity of quantitative branching-time temporal logics
• On the synthesis of strategies in infinite games
• Optimal bounds for multiweighted and parametrised energy games
• Relationships between nondeterministic and deterministic tape complexities
• Temporal specifications with accumulative values

Cited in

(2)

• Synthesis for multi-weighted games with branching-time winning conditions
• Unification and combination of a class of traversal strategies made with pattern matching and fixed-points

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Model checking and synthesis for branching multi-weighted logics

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