Complete Abstractions and Subclassical Modal Logics
In abstract interpretation, the notion of forward-completeness with respect to a logic guarantees that an abstract and a concrete structure satisfy exactly the same formulae. We apply completeness to study models of positive modal logic, which are logics that lack negation and implication. These models, which were discovered independently by re- searchers in abstract interpretation, modal logic and model checking, are Kripke structures with an order on states and their lattice-theoretic duals. We show that forward-complete abstractions are models of certain modal logics. The Kripke structures corresponding to these models satisfy a saturation condition ensuring that modal operators have the same properties as best abstract transformers. We synthesize a new notion of simulation for these models using the constructive characterization of complete abstractions.
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | Abstract InterpretationVMCAI at Amphitheater 44 Chair(s): Roberto Giacobazzi University of Verona, Italy | ||
14:00 30mTalk | Complete Abstractions and Subclassical Modal Logics VMCAI | ||
14:30 30mTalk | Structuring Abstract Interpreters through State and Value Abstractions VMCAI Media Attached | ||
15:00 30mTalk | Conjunctive Abstract Interpretation using Paramodulation VMCAI Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University Media Attached |