A CTL-Based Logic for Program Abstractions

sed Logic for Program Abstractions Martin Lange1 and Markus Latte2 1 Dept. of Computer Science, University of Kassel, Germany 2 Dept. of Computer Science, Ludwig-Maximilians-University Munich, Germany We define an action-based extension of the branching-time temporal logic CTL which allows path quantifiers to be restricted by anguages. The main purpose of this logic is its use in abstract tation. A reduction from a concrete system to an abstract one may contain spurious traces which can render the verification of the abstract system useless with respect to the concrete one. We pick up the on to verify a modified property on the abstract system instead of the one that the concrete system is supposed to have. The logic introduced here enables a systematic modification of such properties. We present some ways of such a modification which aim at implicitly excludious traces in the verification of abstracted systems.

• Type: Conference
• Year: 2010
• Where: WOLLIC
• Authors: Martin Lange, Markus Latte
• Keywords: Artificial Intelligence, Branching-time Temporal Logic, Computer Science, Logic, WOLLIC 2010