Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Personalized HealthCare and Agent Technologies Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

SAT-Versus SMT-Based BMC for TWIS and the Existential Fragment of WCTL with Knowledge

verfasst von : Agnieszka M. Zbrzezny

Erschienen in: Agent and Multi-Agent Systems: Technology and Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this paper, we present the SAT-based bounded model checking method for Timed Weighted Interpreted Systems and for Weighted Existential Computation Tree Logic with epistemic operators. SAT-based bounded model checking consists in translating the existential model checking problem for a modal logic and for a model to the boolean satisfiability problem. We provide an implementation based on Cryptominisat and YicesSAT SAT-solvers and we present a comparison of the SAT-based BMC method and SMT-based BMC methods on common instances that can be scaled up to for performance evaluation.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel An Algorithm for Allocating Structured Tasks in Multi-Robot Scenarios
Nächstes Kapitel Communication and Autonomous Control of Multi-UAV System in Disaster Response Tasks
Literatur
1.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
2.
Dutertre, B.: Yices 2.2. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18–22 July 2014, Proceedings, pp. 737–744 (2014)
3.
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)MATH
4.
Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1–4), 313–328 (2008)MathSciNetMATH
5.
Mȩski, A., Penczek, W., Szreter, M., Woźna-Szcześniak, B., Zbrzezny, A.: BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Auton. Agents Multi-Agent Syst. 28(4), 558–604 (2014)CrossRef
6.
Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRef
7.
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)CrossRef
8.
Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003)MathSciNetMATH
9.
Woźna-Szcześniak, B.: SAT-based bounded model checking for weighted deontic interpreted systems. In: Correia, L., Reis, L.P., Cascalho, J. (eds.) EPIA 2013. LNCS, vol. 8154, pp. 444–455. Springer, Heidelberg (2013)CrossRef
10.
Woźna-Szcześniak, B., Zbrzezny, A.M., Zbrzezny, A.: SAT-based bounded model checking for weighted interpreted systems and weighted linear temporal logic. In: Boella, G., Elkind, E., Savarimuthu, B.T.R., Dignum, F., Purvis, M.K. (eds.) PRIMA 2013. LNCS, vol. 8291, pp. 355–371. Springer, Heidelberg (2013)CrossRef
11.
Wozna-Szczesniak, B.: SAT-based bounded model checking for weighted deontic interpreted systems. Fundam. Inform. 143(1–2), 173–205 (2016)MathSciNetCrossRefMATH
12.
Zbrzezny, A.: Improving the translation from ECTL to SAT. Fundamenta Informaticae 85(1–4), 513–531 (2008)MathSciNetMATH
13.
Zbrzezny, A.M., Zbrzezny, A.: Checking WECTLK properties of timed real-weighted interpreted systems via SMT-based bounded model checking. In: Pereira, F., Machado, P., Costa, E., Cardoso, A. (eds.) EPIA 2015. LNCS, vol. 9273, pp. 638–650. Springer, Cham (2015)
Metadaten
Titel
SAT-Versus SMT-Based BMC for TWIS and the Existential Fragment of WCTL with Knowledge
verfasst von
Agnieszka M. Zbrzezny
Copyright-Jahr
2017
Buch
Agent and Multi-Agent Systems: Technology and Applications

Print ISBN: 978-3-319-59393-7

Electronic ISBN: 978-3-319-59394-4

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-59394-4_11