Model checking of linear-time properties in multi-valued systems

DOI10.1016/J.INS.2016.10.030zbMath1428.68188arXiv1212.2154OpenAlexW2963259237WikidataQ62038065 ScholiaQ62038065MaRDI QIDQ2282319

Lihui Lei, Yong-Ming Li, Manfred Droste

Publication date: 7 January 2020

Published in: Information Sciences (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1212.2154

zbMATH Keywords

livenesssafetyinvariantmodel checkinglattice-valued finite automatonmulti-valued transition system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Many-valued logic (03B50)

Related Items (7)

Unnamed Item ⋮ Fuzzy alternating Büchi automata over distributive lattices ⋮ Fuzzy \(\epsilon\)-approximate regular languages and minimal deterministic fuzzy automata \(\epsilon\)-accepting them ⋮ Quantitative safety and liveness ⋮ Computation tree logic model checking based on multi-valued possibility measures ⋮ Approximate bisimulations and state reduction of fuzzy automata under fuzzy similarity measures ⋮ Fuzzy alternating automata over distributive lattices

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear temporal logic symbolic model checking
• Computation tree logic model checking based on possibility measures
• Finite automata theory with membership values in lattices
• Weighted automata and multi-valued logics over arbitrary bounded lattices
• Fuzzy finite automata and fuzzy regular expressions with membership values in lattice-ordered monoids
• Data structures for symbolic multi-valued model-checking
• An automata-theoretic approach to constraint LTL
• Determinization of weighted finite automata over strong bimonoids
• Defining liveness
• Metamathematics of fuzzy logic
• Reasoning about infinite computations
• Weighted automata and weighted MSO logics for average and long-time behaviors
• Compositional verification and 3-valued abstractions join forces
• Minimization of lattice finite automata and its application to the decomposition of lattice languages
• Fuzzy regular languages over finite and infinite words
• Proving the Correctness of Multiprocess Programs
• Interpolants and Symbolic Model Checking
• Lattice Automata
• Automata theory and its applications
• Model checking of safety properties

This page was built for publication: Model checking of linear-time properties in multi-valued systems