- UHRA Home
- University of Hertfordshire
- Browsing University of Hertfordshire by Author
Browsing University of Hertfordshire by Author "Tveretina, Olga"
Now showing items 1-20 of 23
-
Analyzing Separation of Duties Constraints with a Probabilistic Model Checker
Mendt, Tamara; Sinz, Carsten; Tveretina, Olga (Springer Nature, 2011) -
A BDD-Representation for the Logic of Equality and Uninterpreted Functions
van de Pol, Jaco; Tveretina, Olga (Springer Nature, 2005) -
Binary decision diagrams for first-order predicate logic
Groote, Jan Friso; Tveretina, Olga (2003)Binary decision diagrams (BDDs) are known to be a very efficient technique to handle propositional formulas. We present an extension of BDDs such that they can be used for predicate logic. We define BDDs similar to Bryant ... -
Component Interfaces with Loosely Synchronous Communication
Kirner, Raimund; Maurer, Simon; Tveretina, Olga (Institute of Electrical and Electronics Engineers (IEEE), 2021-08-13)Interface automata have been introduced as a way to advance from value and domain descriptions of type systems to temporal interface descriptions. The original introduction of interface automata used a notion of buffered ... -
Configuring Cloud-Service Interfaces Using Flow Inheritance
Zaichenkov, Pavel; Tveretina, Olga; Shafarenko, Alex (2016-06-01)Technologies for composition of loosely-coupled web services in a modular and flexible way are in high demand today. On the one hand, the services must be flexible enough to be reused in a variety of contexts. On the other ... -
A Constraint Satisfaction Method for Configuring Non-Local Service Interfaces
Zaichenkov, Pavel; Tveretina, Olga; Shafarenko, Alex (Springer Nature, 2016-05-24)Modularity and decontextualization are core principles of a service-oriented architecture. However, the principles are often lost when it comes to an implementation of services due to rigid service interfaces. This paper ... -
The Cost and Benefits of Coordination Programming: Two Case Studies in Concurrent Collection and S-Net
Zaichenkov, Pavel; Gijsbers, Bert; Grelck, Clemens; Tveretina, Olga; Shafarenko, Alex (2016-09-21)This is an evaluation study of the expressiveness provided and the performance delivered by the coordination language S-NET in comparison to Intel’s Concurrent Collections (CnC). An S-NET application is a network of black-box ... -
Deciding Reachability for 3-Dimensional Multi-Linear Systems
Tveretina, Olga (Electronic Proceedings in Theoretical Computer Science, 2011)This paper deals with the problem of point-to-point reachability in multi-linear systems. These systems consist of a partition of the Euclidean space into a finite number of regions and a constant derivative assigned to ... -
Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds
Sandler, Andrei; Tveretina, Olga (Springer, 2019-09-06)A hybrid automaton is a finite state machine combined with some k real-valued continuous variables, where k determines the number of the automaton dimensions. This formalism is widely used for modelling safety-critical ... -
Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds
Sandler, Andrei; Tveretina, Olga (Springer, 2019-09-06)A hybrid automaton is a finite state machine combined with some k real-valued continuous variables, where k determines the number of the automaton dimensions. This formalism is widely used for modelling safety-critical ... -
Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds
Sandler, Andrei; Tveretina, Olga (Springer Nature, 2019-09-06)A hybrid automaton is a finite state machine combined with some k real-valued continuous variables, where k determines the number of the automaton dimensions. This formalism is widely used for modelling safety-critical ... -
A Decision Procedure for Equality Logic with Uninterpreted Functions
Tveretina, Olga (Springer Nature, 2004)The equality logic with uninterpreted functions (EUF) has been proposed for processor verification. A procedure for proving satisfiability of formulas in this logic is introduced. Since it is based on the DPLL method, the ... -
An Exponential Lower Bound on OBDD Refutations for Pigeonhole Formulas
Tveretina, Olga; Sinz, Carsten; Zantema, Hans (2009)Haken proved that every resolution refutation of the pigeonhole formula has at least exponential size. Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has an exponential size. Here ... -
Generalizing DPLL and satisfiability for equalities
Badban, Baharen; van de Pol, Jaco; Tveretina, Olga; Zantema, Hans (2007-08)We present GDPLL, a generalization of the DPLL procedure. It solves the satisfiability problem for decidable fragments of quantifier-free first-order logic. Sufficient conditions are identified for proving soundness, ... -
Interfaces and Concepts to Build Large Resilient and Predictable Systems
Kirner, Raimund; Tveretina, Olga (2019-04-17)Progress in technology not only results in tools of improved capabilities, but also pushes towards integration to create larger systems with unprecedented capabilities. Building such systems with safety-relevant services ... -
Modular Development of Hybrid Systems for Verification in Coq
Niqui, Milad; Tveretina, Olga (Springer Nature, 2008)In this paper we present a formalization of the theory of hybrid automata and algorithms for building trajectory trees using module types and functors in the Coq proof assistant -
Mortality and Edge-to-Edge Reachability are Decidable on Surfaces
de Oliveira Oliveira, Mateus; Tveretina, Olga (ACM Press, 2022-05-04)The mortality problem for a given dynamical system S consists of determining whether every trajectory of S eventually halts. In this work, we show that this problem is decidable for the class of piecewise constant derivative ... -
Non-Local Configuration of Component Interfaces by Constraint Satisfaction
Tveretina, Olga; Zaichenkov, Pavel; Shafarenko, Alex (2020-08-05)Service-oriented computing is the paradigm that utilises services as fundamental elements for developing applications. Service composition, where data consistency becomes especially important, is still a key challenge for ... -
Ordered Binary Decision Diagrams, Pigeonhole Formulas and Beyond
Tveretina, Olga; Sinz, Carsten; Zantema, Hans (2010)Groote and Zantema proved that a particular OBDD computation of the pigeonhole formula has exponential size, and that limited OBDD derivations cannot simulate resolution polynomially. Here we show that an arbitrary OBDD ... -
ParaPlan: A Tool for Parallel Reachability Analysis of Planar Polygonal Differential Inclusion Systems
Sandler, Andrei; Tveretina, Olga (Electronic Proceedings in Theoretical Computer Science, 2017-09-06)We present the ParaPlan tool which provides the reachability analysis of planar hybrid systems defined by differential inclusions (SPDI). It uses the parallelized and optimized version of the algorithm underlying the SPeeDI ...