Model checking computation tree logic over finite lattices

DOI10.1016/j.tcs.2015.10.014zbMath1332.68141OpenAlexW2191419605WikidataQ62038097 ScholiaQ62038097MaRDI QIDQ896917

Zhanyou Ma, Haiyu Pan, Yongzhi Cao, Yong-Ming Li

Publication date: 15 December 2015

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.10.014

zbMATH Keywords

latticemodel checkingweighted automatacomputation tree logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Decidability of the minimization of fuzzy tree automata with membership values in complete lattices, Bisimulations for fuzzy transition systems revisited, Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems, On characterization of fuzzy tree pushdown automata, The relationships among several forms of weighted finite automata over strong bimonoids, TREE AUTOMATA BASED ON COMPLETE RESIDUATED LATTICE-VALUED LOGIC: REDUCTION ALGORITHM AND DECISION PROBLEMS, Multi-valued Verification of Strategic Ability, Lattice-valued tree pushdown automata: pumping lemma and closure properties

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model checking quantum Markov chains
• Multi-valued model checking games
• Computation tree logic model checking based on possibility measures
• Model checking fuzzy computation tree logic
• Finite automata theory with membership values in lattices
• Model-checking in dense real-time
• Weighted automata and multi-valued logics over arbitrary bounded lattices
• Weighted finite automata over strong bimonoids
• Data structures for symbolic multi-valued model-checking
• On model checking multiple hybrid views
• Determinization of weighted finite automata over strong bimonoids
• Automata theory based on quantum logic. I
• The complexity of computing the behaviour of lattice automata on infinite trees
• A theory of computation based on quantum logic. I
• Model checking discounted temporal properties
• Quantitative \(\mu\)-calculus and CTL defined over constraint semirings
• A lattice-theoretical fixpoint theorem and its applications
• Model-Checking Linear-Time Properties of Quantum Systems
• Weighted versus Probabilistic Logics
• DESCRIPTION LOGICS OVER LATTICES
• Lattice Automata
• Automata, Languages and Programming
• Logic Programming
• CONCUR 2003 - Concurrency Theory
• Model checking for a class of weighted automata