Pattern-based refinement of assume-guarantee specifications in reactive synthesis

DOI10.1007/978-3-662-46681-0_49MaRDI QIDQ5194959zbMATH OpenOpenAlexFDO

Authors Salar Moarref, Ufuk Topcu, Rajeev Alur

Publication date 17 September 2019

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-46681-0_49

zbMATH Keywords

label transition systemlinear temporal logicsynthesis problemtransition ruletruth assignment

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Interpolation-based GR(1) assumptions refinement
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Assume-Guarantee Synthesis
• Dependency-Based Compositional Synthesis
• Quantitative assume guarantee synthesis

Cited in

(12)

• Compositional and symbolic synthesis of reactive controllers for multi-agent systems
• Compositional synthesis of modular systems
• A verification-driven framework for iterative design of controllers
• Automated reformulation of specifications by safe delay of constraints
• Interpolation-based GR(1) assumptions refinement
• scientific article; zbMATH DE number 4213463 (Why is no real title available?)
• Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications
• A weakness measure for GR(1) formulae
• A weakness measure for GR(1) formulae
• Dependency-Based Compositional Synthesis
• ACoRe: automated goal-conflict resolution
• Causality-based game solving

This page was built for publication: Pattern-based refinement of assume-guarantee specifications in reactive synthesis

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