Flatness is not a weakness

DOI10.1007/3-540-44622-2_17MaRDI QIDQ2753678zbMATH OpenFDO

Authors Hubert Comon, Véronique Cortier

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44622-2_17

zbMATH Keywords

counter automatalogic in computer sciencemodel-checkingtemporal logicsverifiction

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model-Checking Counting Temporal Logics on Flat Structures
• Taming past LTL and flat counter systems
• Taming past LTL and flat counter systems
• Model checking flat freeze LTL on one-counter automata
• Model checking flat Freeze LTL on one-counter automata

Cited in

(27)

• Pushdown timed automata: A binary reachability characterization and safety verification.
• Well-abstracted transition systems: Application to FIFO automata.
• The complexity of propositional linear temporal logics in simple cases
• Presburger liveness verification of discrete timed automata.
• Eliminating the storage tape in reachability constructions.
• On decidability and complexity of low-dimensional robot games
• Taming past LTL and flat counter systems
• Verification of gap-order constraint abstractions of counter systems
• LTL over integer periodicity constraints
• Verification of gap-order constraint abstractions of counter systems
• Forward analysis and model checking for trace bounded WSTS
• Forward analysis and model checking for trace bounded WSTS
• Some Recent Results in Metric Temporal Logic
• Model checking flat Freeze LTL on one-counter automata
• Constraint LTL satisfiability checking without automata
• The complexity of flat freeze LTL
• scientific article; zbMATH DE number 7559504 (Why is no real title available?)
• The complexity of flat freeze LTL
• An automata-based approach for \(\text{CTL}^{*}\) with constraints
• 5D UED: flat and flavorless
• Taming strategy logic: non-recurrent fragments
• Reasoning about sequences of memory states
• Reasoning about reversal-bounded counter machines
• Constraint LTL with remote access
• On the freeze quantifier in Constraint LTL: Decidability and complexity
• An automata-theoretic approach to constraint LTL
• Verification of qualitative \(\mathbb Z\) constraints

This page was built for publication: Flatness is not a weakness

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