Zobrazeno 1 - 10
of 35
pro vyhledávání: '"Jan-Georg Smaus"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 256, Iss Proc. GandALF 2017, Pp 46-60 (2017)
Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewritin
Externí odkaz:
https://doaj.org/article/796513759fa340cea322383b2b53ff84
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 10, Iss Proc. INFINITY 2009, Pp 36-43 (2009)
We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work which computes new invariants for timed automata con
Externí odkaz:
https://doaj.org/article/050476c40237405eb3307f22e45bc9a5
Publikováno v:
WING@ETAPS/IJCAR
We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We first introduce the CIPM algorithm which computes new invariants for timed automata control loca
Publikováno v:
Electronic Proceedings in Theoretical Computer Science
Proceedings GandALF 2017
8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017)
8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017), Sep 2017, Rome, Italy. pp.46-60, ⟨10.4204/EPTCS.256.4⟩
GandALF
Electronic Proceedings in Theoretical Computer Science, Vol 256, Iss Proc. GandALF 2017, Pp 46-60 (2017)
Electronic proceedings in theoretical computer science, 256
Proceedings GandALF 2017
8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017)
8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017), Sep 2017, Rome, Italy. pp.46-60, ⟨10.4204/EPTCS.256.4⟩
GandALF
Electronic Proceedings in Theoretical Computer Science, Vol 256, Iss Proc. GandALF 2017, Pp 46-60 (2017)
Electronic proceedings in theoretical computer science, 256
Nash equilibrium (NE) is a central concept in game theory. Here we prove formally a published theorem on existence of an NE in two proof assistants, Coq and Isabelle: starting from a game with finitely many outcomes, one may derive a game by rewritin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cfc54ee2f79f5ba2ce7b5d751130adc6
http://arxiv.org/abs/1709.02096
http://arxiv.org/abs/1709.02096
Autor:
Tobias Nipkow, Alexander Schimpf, René Neumann, Peter Lammich, Jan-Georg Smaus, Javier Esparza
Publikováno v:
Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings
25th International Conference on Computer Aided Verification (CAV 2013)
25th International Conference on Computer Aided Verification (CAV 2013), Jun 2013, Saint Petersbourg, Russia. pp.463-478, ⟨10.1007/978-3-642-39799-8_31⟩
[Research Report] Archive of Formal Proofs. 2016
Computer Aided Verification ISBN: 9783642397981
CAV
25th International Conference on Computer Aided Verification (CAV 2013)
25th International Conference on Computer Aided Verification (CAV 2013), Jun 2013, Saint Petersbourg, Russia. pp.463-478, ⟨10.1007/978-3-642-39799-8_31⟩
[Research Report] Archive of Formal Proofs. 2016
Computer Aided Verification ISBN: 9783642397981
CAV
International audience; We present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using recent Isabelle technology called the Re
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e6fadb8f57c89bc38aff897bd12b592a
https://hal.science/hal-03172233
https://hal.science/hal-03172233
Autor:
Pascal Hitzler, Bhaskara Marthi, Anita Raja, Mark O. Riedl, Lilyana Mihalkova, Sriraam Natarajan, David W. Aha, Artur S. d'Avila Garcez, Leslie Pack Kaelbling, Alon Halevy, Robert P. Goldman, Luis C. Lamb, Kristian Kersting, Mark S. Boddy, Vivi Nastase, Gita Sukthankar, Christopher W. Geib, Piotr J. Gmytrasiewicz, Stuart Russell, Stefan Edelkamp, Charles L. Isbell, Jan-Georg Smaus, Darsana P. Josyula, Karl Tuyls, Prashant Doshi, Ron van der Meyden, Keith McGreggor, Ashwin Ram, Gregory Provan, Maithilee Kunda, Ashish Sabharwal, Vadim Bulitko
Publikováno v:
Scopus-Elsevier
Ai Magazine, 31(4), 95-108. AI Access Foundation
AI Magazine; Vol 31, No 4: Winter 2010; 95-108
ResearcherID
Ai Magazine, 31(4), 95-108. AI Access Foundation
AI Magazine; Vol 31, No 4: Winter 2010; 95-108
ResearcherID
The AAAI-10 workshop program was held on July 11-12, 2010, at the Westin Peachtree Plaza in Atlanta, Georgia. The workshop program included 13 workshops covering a wide range of topics in artificial intelligence. There were several presentations on p
Autor:
Jan-Georg Smaus, Alexander Schimpf
Publikováno v:
Logic and Its Applications: 6th Indian Conference, ICLA 2015, Mumbai, India, January 8-10, 2015. Proceedings
6th Indian Conference on Logics and its Applications (ICLA 2015)
6th Indian Conference on Logics and its Applications (ICLA 2015), Jan 2015, Mumbai, India. pp.158-169, ⟨10.1007/978-3-662-45824-2_11⟩
Logic and Its Applications ISBN: 9783662458235
ICLA
6th Indian Conference on Logics and its Applications (ICLA 2015)
6th Indian Conference on Logics and its Applications (ICLA 2015), Jan 2015, Mumbai, India. pp.158-169, ⟨10.1007/978-3-662-45824-2_11⟩
Logic and Its Applications ISBN: 9783662458235
ICLA
International audience; In applications of automata theory, one is interested in reductions in the size of automata that preserve the recognised language. For Büchi automata, two optimisations have been proposed: bisimulation reduction, which comput
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5db423e1227ba91cf372c4f67e97ce09
https://oatao.univ-toulouse.fr/18943/
https://oatao.univ-toulouse.fr/18943/
Autor:
Stefan Ratschan, Jan-Georg Smaus
Publikováno v:
ADHS
This paper provides a method for coupling safety verification algorithms for non-deterministic (and, in general, non-linear) hybrid systems with the ability of finding concrete counterexamples, i.e., with falsification. Such a tight integration of ve
Publikováno v:
Theory and Practice of Logic Programming. 2:369-418
Termination of logic programs depends critically on the selection rule, i.e. the rule that determines which atom is selected in each resolution step. In this article, we classify programs (and queries) according to the selection rules for which they
Publikováno v:
Information and Communication Technologies in Education, Research, and Industrial Applications-11th International Conference, ICTERI 2015, Lviv, Ukraine, May 14-16, 2015, Revised Selected Papers
11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015)
11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015), May 2015, Lviv, Ukraine. pp.109-123, ⟨10.1007/978-3-319-30246-1_7⟩
Information and Communication Technologies in Education, Research, and Industrial Applications ISBN: 9783319302454
ICTERI
11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015)
11th International Conference onICT in Education, Research, and Industrial Applications (ICTERI 2015), May 2015, Lviv, Ukraine. pp.109-123, ⟨10.1007/978-3-319-30246-1_7⟩
Information and Communication Technologies in Education, Research, and Industrial Applications ISBN: 9783319302454
ICTERI
International audience; There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of finite automata, so defining an abstraction mapping from semantics to automata and provin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9d5d842b7fe9dbaf6d421e48e4e0c266
http://arxiv.org/abs/1409.7841
http://arxiv.org/abs/1409.7841