Verification of non-regular program properties [Elektronische Ressource] / vorgelegt von Roland Axelsson

Verification of Non-Regular ProgramPropertiesRoland AxelssonMu¨nchen 2010Verification of Non-Regular ProgramPropertiesRoland AxelssonDissertationam Institut fu¨r InformatikLudwig–Maximilians–Universit¨atMu¨nchenvorgelegt vonRoland AxelssonMu¨nchen, den 27.4.2010Erstgutachter: Prof. Dr. Martin LangeZweitgutachter: Prof. Dr. Thomas WilkeTag der mu¨ndlichen Pru¨fung: 25.6.2010AbstractMost temporal logics which have been introduced and studied in the past decades can be∗embedded into the modalL . This is the case for e.g. PDL, CTL, CTL , ECTL, LTL,etc. and entails that these logics cannot express non-regular program properties. In recentyears, some novel approaches towards an increase in expressive power have been made:Fixpoint Logic with Chop enrichesL with a sequential composition operator and therebyallows to characterise context-free processes. The Modal Iteration Calculus uses inflation-ary fixpoints to exceed the expressive power ofL . Higher-Order Fixpoint Logic (HFL)incorporates a simply typedλ-calculus into a setting with extremal fixpoint operators andeven exceeds the expressive power of Fixpoint Logic with Chop. But also PDL has beenequipped with context-free programs instead of regular ones.In terms of expressivity there is a natural demand for richer frameworks since programproperty specifications are simply not limited to the regular sphere.