LTL with arithmetic and its applications in reasoning about hierarchical systems

DOI10.29007/WPG3zbMATH Open1415.68144OpenAlexW2907493568MaRDI QIDQ5222965FDOQ5222965

Authors: Rachel Faran, Orna Kupferman 

Publication date: 4 July 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.29007/wpg3

Recommendations

• Improved model checking of hierarchical systems
• Improved model checking of hierarchical systems
• Extending temporal logics with data variable quantifications
• Taming past LTL and flat counter systems
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints

zbMATH Keywords

integer linear programmingmodel checkinghierarchical systemsinfinite alphabetsLTL with arithmetic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cited In (4)

• SEPARATING AUXILIARY ARITY HIERARCHY OF FIRST-ORDER INCREMENTAL EVALUATION SYSTEMS USING (3K+1)-ary INPUT RELATIONS
• Realizability modulo theories
• On Synthesis of Specifications with Arithmetic
• Boolean abstractions for realizability modulo theories

This page was built for publication: LTL with arithmetic and its applications in reasoning about hierarchical systems

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