Model checking computation tree logic over finite lattices

DOI10.1016/J.TCS.2015.10.014zbMATH Open1332.68141DBLPjournals/tcs/PanLCM16OpenAlexW2191419605WikidataQ62038097 ScholiaQ62038097MaRDI QIDQ896917FDOQ896917

Authors: Haiyu Pan, Yongzhi Cao, Zhanyou Ma, Yongming 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

Recommendations

• Computation tree logic model checking based on multi-valued possibility measures
• scientific article; zbMATH DE number 2042616
• Automata, Languages and Programming
• Multi-valued model checking via classical model checking.
• Model checking for nondeterministic multi-valued Kripke structures

zbMATH Keywords

latticemodel checkingcomputation tree logicweighted automata

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (15)

• Computation tree logic model checking based on multi-valued possibility measures
• Model checking for nondeterministic multi-valued Kripke structures
• TREE AUTOMATA BASED ON COMPLETE RESIDUATED LATTICE-VALUED LOGIC: REDUCTION ALGORITHM AND DECISION PROBLEMS
• Quantitative analysis of lattice-valued Kripke structures
• On characterization of fuzzy tree pushdown automata
• Model Checking Quantified Computation Tree Logic
• Title not available (Why is that?)
• 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
• Automata, Languages and Programming
• The relationships among several forms of weighted finite automata over strong bimonoids
• Coalgebraic CTL: fixpoint characterization and polynomial-time model checking
• Lattice-valued tree pushdown automata: pumping lemma and closure properties
• Multi-valued verification of strategic ability

This page was built for publication: Model checking computation tree logic over finite lattices

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