First-Order and Temporal Logics for Nested Words
From MaRDI portal
Publication:3623007
DOI10.2168/LMCS-4(4:11)2008zbMath1159.03018WikidataQ56912298 ScholiaQ56912298MaRDI QIDQ3623007
Kousha Etessami, Neil Immerman, Marcelo Arenas, Pablo Barceló, Rajeev Alur, Leonid O. Libkin
Publication date: 29 April 2009
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Logic in computer science (03B70) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
A Branching Time Variant of CaRet, Model-checking structured context-free languages, Model checking dynamic memory allocation in operating systems, Model Checking Procedural Programs, First-Order Logic Definability of Free Languages, The complexity of model checking multi-stack systems, Visibly pushdown transducers, Operator Precedence Languages: Their Automata-Theoretic and Logic Characterization, Verification of programs with exceptions through operator precedence automata, Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages, Model Checking Temporal Properties of Recursive Probabilistic Programs, Evolving schemas for streaming XML, Generalizing input-driven languages: theoretical and practical benefits, Unnamed Item, Regular languages of nested words: fixed points, automata, and synchronization, Operator precedence temporal logic and model checking, Temporal logics for concurrent recursive programs: satisfiability and model checking, Verifying quantitative temporal properties of procedural programs, Hybrid and First-Order Complete Extensions of CaRet, Visibly linear temporal logic, Visibly pushdown modular games, Weighted automata and logics for infinite nested words, Temporal logics with language parameters, Toward a theory of input-driven locally parsable languages, Unnamed Item, CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties, Realizability of Concurrent Recursive Programs, State Complexity of Nested Word Automata, ProMoVer: Modular Verification of Temporal Safety Properties
Uses Software
