Model checking computation tree logic over finite lattices

DOI10.1016/J.TCS.2015.10.014MaRDI QIDQ896917zbMATH OpenOpenAlexDBLPWikidataFDO

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

zbMATH Keywords

latticemodel checkingcomputation tree logicweighted automata

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(15)

• Computation tree logic model checking based on multi-valued possibility measures
• Bisimulations for fuzzy transition systems revisited
• scientific article; zbMATH DE number 2042616 (Why is no real title available?)
• Decidability of the minimization of fuzzy tree automata with membership values in complete lattices
• On characterization of fuzzy tree pushdown automata
• Automata, Languages and Programming
• Lattice-valued tree pushdown automata: pumping lemma and closure properties
• Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems
• Quantitative analysis of lattice-valued Kripke structures
• TREE AUTOMATA BASED ON COMPLETE RESIDUATED LATTICE-VALUED LOGIC: REDUCTION ALGORITHM AND DECISION PROBLEMS
• Model Checking Quantified Computation Tree Logic
• Multi-valued verification of strategic ability
• Model checking for nondeterministic multi-valued Kripke structures
• The relationships among several forms of weighted finite automata over strong bimonoids
• Coalgebraic CTL: fixpoint characterization and polynomial-time model checking

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)