Model checking of linear-time properties in multi-valued systems
From MaRDI portal
Publication:2282319
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
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
Cites Work
- 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
- 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
This page was built for publication: Model checking of linear-time properties in multi-valued systems