Zobrazeno 1 - 10
of 25
pro vyhledávání: '"Frenkel, Hadar"'
Publikováno v:
Computer Aided Verification: 36th International Conference, CAV 2024, Proceedings, Part III, Lecture Notes in Computer Science, vol 14683, Springer
We present an automata-based algorithm to synthesize omega-regular causes for omega-regular effects on executions of a reactive system, such as counterexamples uncovered by a model checker. Our theory is a generalization of temporal causality, which
Externí odkaz:
http://arxiv.org/abs/2405.10912
Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge, information flow, and privac
Externí odkaz:
http://arxiv.org/abs/2404.09652
Autor:
Frenkel, Hadar, Zimmermann, Martin
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are as hard as truth in third-order arithmetic. We also consider two fragments of second-order HyperLTL that have been int
Externí odkaz:
http://arxiv.org/abs/2311.15675
We introduce Hyper$^2$LTL, a temporal logic for the specification of hyperproperties that allows for second-order quantification over sets of traces. Unlike first-order temporal logics for hyperproperties, such as HyperLTL, Hyper$^2$LTL can express c
Externí odkaz:
http://arxiv.org/abs/2305.17935
We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory cells, functions and predicates, making it a convenient and expressiv
Externí odkaz:
http://arxiv.org/abs/2303.14796
Autor:
Frenkel, Hadar, Sheinvald, Sarai
Publikováno v:
EPTCS 370, 2022, pp. 114-130
Hyperproperties lift conventional trace-based languages from a set of execution traces to a set of sets of executions. From a formal-language perspective, these are sets of sets of words, namely hyperlanguages. Hyperautomata are based on classical au
Externí odkaz:
http://arxiv.org/abs/2209.10306
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like program
Externí odkaz:
http://arxiv.org/abs/2207.10534
Autor:
Coenen, Norine, Dachselt, Raimund, Finkbeiner, Bernd, Frenkel, Hadar, Hahn, Christopher, Horak, Tom, Metzger, Niklas, Siber, Julian
Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces as a counterexample. Fixing the erroneous relations between traces in
Externí odkaz:
http://arxiv.org/abs/2206.02074
Publikováno v:
Logical Methods in Computer Science, Volume 19, Issue 2 (April 20, 2023) lmcs:8899
We study the learnability of symbolic finite state automata (SFA), a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all obtained results
Externí odkaz:
http://arxiv.org/abs/2112.14252
We revisit the complexity of procedures on SFAs (such as intersection, emptiness, etc.) and analyze them according to the measures we find suitable for symbolic automata: the number of states, the maximal number of transitions exiting a state, and th
Externí odkaz:
http://arxiv.org/abs/2011.05389