Sun 23 Jun 2019 14:00 - 14:30 at 212B - Session III Chair(s): Max Schaefer

Both Datalog and Computation Tree Logic (CTL) model checking have been used for declaratively analysing programs. Gottlob et al. (2002) shows how to translate CTL formulae to a subset of Datalog. We extend this by embedding multimodal CTL into the wider Datalog language so that they can be used side-by-side. Further, we extend Datalog with temporal hybrid logic operators to be able to reify and modify the hidden (implicit) time used by the CTL operators in a structured manner. Our system is entirely time agnostic: different notions of time such as a program counter, nodes of a dataflow graph, or versions of software repositories can all be used. Multimodal CTL operators allow various notions of time to be used together within the same clause. We compile our extension into stratified Datalog while preserving properties such as domain independence and well-modedness.

Sun 23 Jun

14:00 - 15:30: DPA - Session III at 212B
Chair(s): Max SchaeferGitHub
dpa-2019-papers14:00 - 14:30
Mistral ContrastinUniversity of Cambridge, UK
dpa-2019-papers14:30 - 15:00
Manuel HermenegildoIMDEA Software Institute and T.U. of Madrid (UPM)
dpa-2019-papers15:00 - 15:30
Thomas GilrayThe University of Alabama at Birmingham