1 citations · 2 across the 6 of their papers we have counts for
7 papers
A Complexity Bound for Determinisation of Min-Plus Weighted Automata
Shaull Almagor, Guy Arbel, Sarai Sheinvald
The determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-construct…
Unambiguisability and Register Minimisation of Min-Plus Models
Shaull Almagor, Guy Arbel, Sarai Sheinvald
We study the unambiguisability problem for min-plus (tropical) weighted automata (WFAs), and the counter-minimisation problem for tropical Cost Register Automata (CRAs), which are…
Determinization of Min-Plus Weighted Automata is Decidable
Shaull Almagor, Guy Arbel, Sarai Sheinvald
We show that the determinization problem for min-plus (tropical) weighted automata is decidable, thus resolving this long-standing open problem. In doing so, we develop a new toolb…
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Tzu-Han Hsu, César Sánchez, Sarai Sheinvald +1
Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite str…
Realizable and Context-Free Hyperlanguages
Hadar Frenkel, Sarai Sheinvald
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…
Finite-Word Hyperlanguages
Borzoo Bonakdarpour, Sarai Sheinvald
Formal languages are in the core of models of computation and their behavior. A rich family of models for many classes of languages have been widely studied. Hyperproperties lift c…
Automata for Hyperlanguages
Borzoo Bonakdarpour, Sarai Sheinvald
Hyperproperties lift conventional trace properties from a set of execution traces to a set of sets of execution traces. Hyperproperties have been shown to be a powerful formalism f…