Visibly linear dynamic logic

DOI10.1016/J.TCS.2018.06.030MaRDI QIDQ1786616zbMATH OpenOpenAlexWikidataFDO

Authors Alexander Weinert, Martín G. Zimmermann

Publication date 24 September 2018

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1512.05177, https://drops.dagstuhl.de/opus/volltexte/2016/6863/

zbMATH Keywords

infinite gamesmodel checkingsatisfiabilitytemporal logicvisibly pushdown languages

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We introduce Visibly Linear Dynamic Logic (VLDL), which extends Linear Temporal Logic (LTL) by temporal operators that are guarded by visibly pushdown languages over finite words. In VLDL one can, e.g., express that a function resets a variable to its original value after its execution, even in the presence of an unbounded number of intermediate recursive calls. We prove that VLDL describes exactly the $omega$-visibly pushdown languages. Thus it is strictly more expressive than LTL and able to express recursive properties of programs with unbounded call stacks. The main technical contribution of this work is a translation of VLDL into $omega$-visibly pushdown automata of exponential size via one-way alternating jumping automata. This translation yields exponential-time algorithms for satisfiability, validity, and model checking. We also show that visibly pushdown games with VLDL winning conditions are solvable in triply-exponential time. We prove all these problems to be complete for their respective complexity classes.

Recommendations

• Visibly linear dynamic logic
• Visibly linear temporal logic
• Visibly linear temporal logic
• VLDL satisfiability and model checking via tree automata
• Propositional dynamic logic with recursive programs

Cites work

• Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• Parametric linear dynamic logic
• Programming Techniques: Regular expression search algorithm
• Reachability analysis of pushdown automata: Application to model-checking
• Reasoning about infinite computations
• Regular Linear Temporal Logic
• Temporal logic can be more expressive
• Tools and Algorithms for the Construction and Analysis of Systems
• Visibly linear dynamic logic
• Visibly linear temporal logic
• Visibly pushdown languages
• Visibly rational expressions
• VLDL satisfiability and model checking via tree automata

Cited in

(11)

• Temporal logics with language parameters
• Visibly linear temporal logic
• Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages
• Visibly linear dynamic logic
• VLDL satisfiability and model checking via tree automata
• Parametric linear dynamic logic
• A fixpoint calculus for local and global program flows
• Temporal logics with language parameters
• Visibly linear temporal logic
• Automata-theoretic characterisations of branching-time temporal logics
• A note on an extension of PDL

Describes a project that uses

Uses Software

• MOPS

This page was built for publication: Visibly linear dynamic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1786616)