Invariant Inference and Complexity Analysis in Transition Systems
Explore the complexities of invariant inference in transition systems, delving into topics such as safety, inductive invariants, SAT-based inference algorithms, and the exact learning model. Discover how these methods succeed, fail, and potential enhancements for better results.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Complexity and Information in Invariant Inference Yotam Feldman Neil Immerman Mooly Sagiv Sharon Shoham @yotamfe, @SagivMooly @yotamfe, @SagivMooly
Safety of Transition Systems Bad Reach Initial
Inductive Invariants inductiveness Bad Inv TR Reach initial not bad Initial
Inductive Invariants: Example ?: Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ?: (?1, ,??) 1 1 Not inductive: 00 1 11 1 ? ? ? ?: ?? 1 Inductive: ?? 1 ? ?
SAT-Based Inference Algorithms Goal: find inductive invariants automatically Means: employ a SAT solver predicate abstraction [CAV 97, POPL 02] symbolic abstraction [VMCAI 04, 16] interpolation [CAV 03,TACAS 06] IC3/PDR [VMCAI 11, FMCAD 11] abduction [OOPSLA 13] SyGuS [FMCAD 13, ] ICE learning [CAV 14, POPL 15] Why do they succeed? Why do they fail? (How can we make them better?)
This Work Complexity of SAT-based invariant inference in amodel of exact learning with queries
Problem Setting: Polynomial-Length Inference Boolean transition systems, = ?1, ,?? Given a transition system from a class ? (over ), Find an inductive invariant ? CNF ? poly(?) ?-complete.) (Decision problem is 2
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? ? = 00 1, ? = 1 1 Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? ? = 00 1, ? = 1 1 `` Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? generalize ? = 00 1, ? = 1 1 PDR-1: drop literals from ? while {Init}?{ ?} Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ?1= 0 ?2= 0 ??= 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? generalize ? = 00 1, ? = 1 1 PDR-1: drop literals from ? while {Init}?{ ?} Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ?1= 0 ?2= 0 ??= 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? generalize ? = 00 1, ? = 1 1 PDR-1: drop literals from ? while {Init}?{ ?} Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ?1= 0 ?2= 0 ??= 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? generalize ? = 00 1, ? = 1 1 PDR-1: drop literals from ? while {Init}?{ ?} Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ?1= 0 ?2= 0 ??= 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? generalize ? = 00 1, ? = 1 1 PDR-1: drop literals from ? while {Init}?{ ?} Init
Example: PDR-1 ? : Init: ?1, ,?? ?1, ,?? ?1, ,?? + 2 (?1, ,??)(mod 2?) (?1, ,??) 0 0 Bad: (?1, ,??) = 1 1 ?1= 0 ?2= 0 ??= 1 ? = ?1= 1 ?2= 1 ??= 1 Bad ? ? generalize ? = 00 1, ? = 1 1 PDR-1: drop literals from ? while {Init}?{ ?} ? = ?1= 1 ?2= 1 ??= 1 (??= 1) Init
Example: PDR-1 inductiveness check I := Bad while !{I}?{I}: ?,? := CTI(?,I) I := I ??????????( ?) ??????????( ?): drop literals from ? while {Init}?{ ?} Hoare check V
Main Results inference is hard in general I := Bad while !{I}?{I}: ?,? := CTI(?,I) I := I ??????????( ?) but rich checks ? ?{?} beyond inductiveness ? ? ? can be powerful ??????????( ?): drop literals from ? while {Init}?{ ?}
Hoare-Query Model Capable of modeling PDR inference algorithm Hoare-query oracle {?1} ?1? / {??} {??} ? {??} ??? / Algorithms cannot access the transition relation directly, only perform Hoare queries
Hoare-Query Model Capable of modeling PDR Hoare-query oracle PDR-1 {I} I ? / I := Bad while !{I}?{I}: ?,? := CTI(?,I) I := I ??????????( ?) {??} {??} ? model of {I}?{I}, ?(?) queries Init { ?}? / ??????????( ?): drop literals from ? while {Init}?{ ?}
Hoare-Query Complexity Complexity: # Hoare queries Hoare-query oracle PDR-1 {I} I ? / I := Bad while !{I}?{I}: ?,? := CTI(?,I) I := I ??????????( ?) {??} {??} ? model of {I}?{I}, ?(?) queries Init { ?}? / ??????????( ?): drop literals from ? while {Init}?{ ?}
Hoare-Query Complexity Complexity: # Hoare queries Thm: Every Hoare-query algorithm requires ??(?) Hoare-queries in the worst case. (? is the vocabulary size) even with unlimited computational power unconditional lower bound but rich Hoare-queries ? ? ? can be powerful
Inductiveness-Query Model A special case of the Hoare-query model closely related to ICE learning [CAV 14] inductiveness-query oracle inference algorithm ?1 inductive? / +counterexample ?? inductive? / +counterexample {??} {??} ? Complexity: # inductiveness queries worst caseamongst possible counterexamples [CAV 14] ICE: A Robust Framework for Learning Invariants. Pranav Garg, Christof L ding, P. Madhusudan, Daniel Neider.
Hoare > Inductiveness Thm: There exists a class of transition systems ?, so that for solving polynomial-length inference: 1. Hoare-query algorithm with poly(?)queries 2. inductiveness-query algorithm requires 2 (?) queries a simple case of PDR ICE cannot model PDR, and the extension of [VMCAI 17] is necessary [VMCAI 17] IC3 - Flipping the E in ICE. Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik.
Hoare > Inductiveness Thm: There exists a class of transition systems ?, so that for solving polynomial-length inference: 1. Hoare-query algorithm with poly(?)queries 2. inductiveness-query algorithm requires 2 (?) queries PDR-1 I := Bad while !{I}?{I}: ?,? := CTI(?,I) I := I ??????????( ?) ??????????( ?): drop literals from ? while {Init}?{ ?}
Hoare > Inductiveness Thm: Exists a class of transition systems ?, so that for solving polynomial-length inference: 1. Hoare-query algorithm with poly(?)queries 2. inductiveness-query algorithm requires 2 (?) queries Proof: monotone CNF with ? clauses propositions appear only negatively ? = ?1 ( ?2 ?3)
Hoare > Inductiveness Thm: Exists a class of transition systems ?, so that for solving polynomial-length inference: 1. Hoare-query algorithm with poly(?)queries 2. inductiveness-query algorithm requires 2 (?) queries Proof: ?= maximal transition systems for monotone CNF with ? clauses propositions appear only negatively ? = ?1 ( ?2 ?3) Maximal system for ?:
Hoare > Inductiveness Upper bound: Hoare-query algorithm with poly(?)queries PDR-1 takes ?(??) queries Proof: ??????????( ?): drop literals from ? while {Init}?{ ?} ? ? 1 iteration 1 iteration ? is minimal ? = ?1 ( ?2 ?3) monotone
Hoare > Inductiveness Lower bound: inductiveness-query algorithm requires 2 (?) queries Proof: inductiveness-query oracle inference algorithm ?1 inductive? +counterexample ?? inductive? +counterexample {??} {??} ? ? ? ??? ?? ??
Hoare > Inductiveness Lower bound: inductiveness-query algorithm requires 2 (?) queries Proof: Thm: invariants in monotone CNF maximal systems monotone CNF invariants general systems monotone CNF invariants ? ? ??? 2 (?)
Hoare > Inductiveness Thm: There exists a class of transition systems ?, so that for solving polynomial-length inference: 1. Hoare-query algorithm with poly(?)queries 2. inductiveness-query algorithm requires 2 (?) queries Thm: Learning from counterexamples to induction is harder than learning from examples labeled positive/negative.
Conclusion Complexity of inferring polynomial-length invariants Hoare-query model: ? ?{?} Thm 1: Exponential number of Hoare-queries required in general Thm 2: Power of ? ? ? (Hoare) > power of ? ? ? (ICE) Thm 3: Power of CTIs (?,? )< power of labeled ?+,?
