Academic
Publications
A Temporal Logic of Nested Calls and Returns

A Temporal Logic of Nested Calls and Returns,Rajeev Alur,Kousha Etessami,P. Madhusudan

A Temporal Logic of Nested Calls and Returns   (Citations: 77)
BibTex | RIS | RefWorks Download
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...There are interesting temporal logics suitable for expressing properties of single-stack pushdown systems, like the logic CARET [4])...

    P. Madhusudanet al. The tree width of auxiliary storage

    • ...For instance, model checking regular nested-word properties of recursive state machines, which can model control flows of imperative programs [3, 4], and of Boolean programs [7], which are widely used as abstractions in software model checking, can be carried out in an automata-theoretic setting, similar to finite-state model checking [23]...
    • ...a formula in a temporal logic over nested words like CaRet [4], NWTL [2], and μNWTL [10], is translated into a language-equivalent NWA...
    • ...In [2, 4], the respective authors introduce the temporal logics CaRet and...

    Christian Daxet al. Alternation Elimination for Automata over Nested Words

    • ...Such structures naturally appear in XML documents that are string representations of trees using opening and closing tags [8, 32], or in software verification of programs with stack-based control flow [2, 4]. A nested word automaton [6] runs from left to right, similarly to a finite state automaton, but each time it encounters a “return” position, the next state depends not only on the current state but also on the state of the matching ...
    • ...Applications in program analysis are discussed, e.g., in [2, 4], and applications in processing treestructured data in [8, 32]...
    • ...With the development of temporal logics for nested words [1, 2, 4], it is natural to develop alternating automata for nested words, with the hope that they can simplify the process of translating temporal logics into automata...

    Marcelo Arenaset al. Regular Languages of Nested Words: Fixed Points, Automata, and Synchro...

    • ...The benets of this modeling have already been shown for software model checking: when all variables are boolean, viewing the program as a nite-state nested-word-automaton generating a regular language of nested words allows model checking of non-regular temporal properties [2, 1, 6]...
    • ...In a nested word, there are many notions of paths such as global, local, and staircase [2, 1, 13]|temporal logics for nested words contain modalities such as \always" and \eventually" parameterized by the path type...
    • ...There have been many papers on nested words and associated logics recently, but these focus on model checking (of pushdown models) and expressiveness [13, 2, 1, 6]...

    Rajeev Aluret al. Temporal Reasoning for Procedural Programs

    • ...Researchers then considered more expressive logics that are tailored for pushdown graphs [AEM04] 1 and showed how to handle restricted cases of communicating pushdown systems [KIG05, BTP06, KG06, KGS06, KG07]...
    • ...It can be easily extended to handle also CARET specifications [AEM04]...
    • ...Recently, Alur et al. suggested the logic CARET, that can specify non-regular properties [AEM04]...

    Orna Kupfermanet al. An Automata-Theoretic Approach to Infinite-State Systems

Sort by: