Zobrazeno 1 - 10
of 29
pro vyhledávání: '"Karin Quaas"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 15, Issue 3 (2019)
We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one ano
Externí odkaz:
https://doaj.org/article/e35682648a1e41998bc70cdd1d91d4c9
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 3 (2017)
Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checkin
Externí odkaz:
https://doaj.org/article/8b7c1dd7d83b425988326731c5149291
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 151, Iss Proc. AFL 2014, Pp 174-187 (2014)
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent extensions of Linear Temporal Logic to specify properties about data languages. In this paper, we consider the class of data languages of non-monotonic data words
Externí odkaz:
https://doaj.org/article/2ee98efeb6694264a6a350c9b1d28895
Autor:
Karin Quaas
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 145, Iss Proc. SynCoP 2014, Pp 5-17 (2014)
Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 1993 by Alur, Henzinger, and Vardi, it is known that the emptiness proble
Externí odkaz:
https://doaj.org/article/115dd3a9ccff47c7890a5275997865aa
Autor:
Karin Quaas
Publikováno v:
Logical Methods in Computer Science, Vol Volume 11, Issue 3 (2015)
We study decidability of verification problems for timed automata extended with unbounded discrete data structures. More detailed, we extend timed automata with a pushdown stack. In this way, we obtain a strong model that may for instance be used to
Externí odkaz:
https://doaj.org/article/0db1ea88824e4e73993000e2b78db94f
Autor:
Karin Quaas, Stéphane Demri
Publikováno v:
ACM SIGLOG News
ACM SIGLOG News, ACM, 2021, 8 (3), pp.6-29. ⟨10.1145/3477986.3477988⟩
ACM SIGLOG News, 2021, 8 (3), pp.6-29. ⟨10.1145/3477986.3477988⟩
ACM SIGLOG News, ACM, 2021, 8 (3), pp.6-29. ⟨10.1145/3477986.3477988⟩
ACM SIGLOG News, 2021, 8 (3), pp.6-29. ⟨10.1145/3477986.3477988⟩
International audience; In this short survey, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These include temporal logics with concrete domains, description logics with concrete d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::129ea1cb5891db3e01aa986b7daf1e88
https://hal.archives-ouvertes.fr/hal-03313291
https://hal.archives-ouvertes.fr/hal-03313291
Publikováno v:
ACM Transactions on Computational Logic. 21:1-34
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are quantitative extensions of Linear Temporal Logic (LTL) that are prominent and widely used in the verification of real-timed systems. We study MTL and TPTL as specification
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::30436f1613bfd05cf4728da65bf15ebd
https://doi.org/10.1145/3372789
https://doi.org/10.1145/3372789
Publikováno v:
Fahrenberg, U, Legay, A & Quaas, K 2020, ' Computing branching distances with quantitative games ', Theoretical Computer Science, vol. 847, pp. 134-146 . https://doi.org/10.1016/j.tcs.2020.10.001
Theoretical Computer Science, Vol. 847, no.847, p. 134-146 (2020)
Theoretical Computer Science, Vol. 847, no.847, p. 134-146 (2020)
We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of qua
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6199fdb3fe64d0b2fd53162efd3be4a1
https://vbn.aau.dk/da/publications/6a436712-c3fc-422f-9fba-dc4bb7fd4c93
https://vbn.aau.dk/da/publications/6a436712-c3fc-422f-9fba-dc4bb7fd4c93
Autor:
Antoine Mottet, Karin Quaas
Publikováno v:
Theory of Computing Systems
We investigate the complexity of the containment problem “Does $L(\mathcal {A})\subseteq L({\mathscr{B}})$ hold?” for register automata and timed automata, where ${\mathscr{B}}$ is assumed to be unambiguous and $\mathcal {A}$ is arbitrary. We pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::193dcdf8891fff020b3a7b0e799abd69
Publikováno v:
Acta Cybernetica, Vol. 23, no.1, p. 203-228 (2017)
Energy problems are important in the formal analysis of embedded or autonomous systems. With the purpose of unifying a number of approaches to energy problems found in the literature, we introduce energy automata. These are finite automata whose edge
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::24c68e2ecf0a279e736064f69e382b1a
https://doi.org/10.14232/actacyb.23.1.2017.13
https://doi.org/10.14232/actacyb.23.1.2017.13