Back to Search
Start Over
Model checking against arbitrary public announcement logic: A first-order-logic prover approach for the existential fragment
- Source :
- DALI@TABLEAUX, DALI@TABLEAUX, 2017, Brasília, Brazil, Lecture Notes in Computer Science ISBN: 9783319735788
- Publication Year :
- 2017
- Publisher :
- HAL CCSD, 2017.
-
Abstract
- International audience; In this paper, we investigate the model checking problem of symbolic models against epis-temic logic with arbitrary public announcements and group announcements. We reduce this problem to the satisfiability of Monadic Monadic Second Order Logic (MMSO), the fragment of monadic-second order logic restricted to monadic predicates. In particular, for the case of epistemic formulas in which all arbitrary and group announcements are existential, the proposed reduction lands in monadic first-order logic. We take advantage of this situation to report on few experiments we made with first-order provers.
- Subjects :
- Model checking
Reduction (recursion theory)
Group (mathematics)
Computer science
0102 computer and information sciences
02 engineering and technology
Gas meter prover
16. Peace & justice
01 natural sciences
Satisfiability
First-order logic
[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Epistemic modal logic
Fragment (logic)
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Mathematics::Category Theory
Computer Science::Logic in Computer Science
0202 electrical engineering, electronic engineering, information engineering
Calculus
020201 artificial intelligence & image processing
Computer Science::Formal Languages and Automata Theory
Subjects
Details
- Language :
- English
- ISBN :
- 978-3-319-73578-8
- ISBNs :
- 9783319735788
- Database :
- OpenAIRE
- Journal :
- DALI@TABLEAUX, DALI@TABLEAUX, 2017, Brasília, Brazil, Lecture Notes in Computer Science ISBN: 9783319735788
- Accession number :
- edsair.doi.dedup.....2487abb1380ba599b9a920bfe8fa27bb