1,721,003 research outputs found
Hybrid Automata and Bisimulation
No full textThis paper surveys hybrid automata and bisimulation relations. We formally introduce both notions and briefly present the model
checking problem over hybrid automata. We show how, in some cases, bisimulations can be used to quotient infinite state systems to finite ones and, hence, we reduce the model checking over hybrid automata to model checking over finite models. Finally, we review some classes of hybrid automata which admit finite bisimulation quotients
Is Hyper-extensionality Preservable Under Deletions of Graph Elements?
Full text linkAny hereditarily finite set S can be represented as a finite pointed graph –dubbed membership graph– whose nodes denote elements of the transitive closure of {S} and whose edges model the membership relation. Membership graphs must be hyper-extensional, that is pairwise distinct nodes are not bisimilar and (uniquely) represent hereditarily finite sets.
We will see that the removal of even a single node or edge from a membership graph can cause “collapses” of different nodes and, therefore, the loss of hyper-extensionality of the graph itself. With the intent of gaining a deeper understanding on the class of hyper-extensional hereditarily finite sets, this paper investigates whether pointed hyper-extensional graphs always contain either a node or an edge whose removal does not disrupt the hyper-extensionality property
Family Fingerprints: A Global Approach to Structural Classification
No full textProtein domain classification is a useful instrument to deduce functional properties of proteins. Many automatic tools to classify domains according to available databases have been proposed so far. This paper introduces the notion of "fingerprint" as an easy and readable digest of the similarities between a protein fragment and an entire set of sequences, and this concept offers us a rationale for building an automatic SCOP classifier which assigns a query sequence to the most likely family. Fingerprint-based analysis has been implemented in a software tool and we report some experimental validations for it
Unwinding biological systems
Full text linkUnwinding conditions have been fruitfully exploited in Information Flow Security to define persistent security properties. In this paper we investigate their meaning and possible uses in the analysis of biological systems. In particular, we elaborate on the notion of robustness and propose some instances of unwinding over the process algebra Bio-PEPA and over hybrid automata. We exploit such instances to analyse two case-studies: Neurospora crassa circadian system and Influenza kinetics models. © 2015 Elsevier B.V
Model-based tumour subclonal deconvolution accounting for spatio-temporal sampling biases
No full textBulk DNA sequencing has entered the clinic, and understanding tumour evolution in space and time has become critical for advancing precision oncology. A recent work by us has brought a population genetics perspective into the classical tumour subclonal deconvolution problem, showing how multiple spatiotemporal sampling biases arise when we collect more than one sample of the same tumour. Sampling biases complicate the mapping of the mutations into the evolutionary process, a complex issue undermined by existing multi-sample analysis methods. This work presents MOBSTERm, a novel mixture-within-mixture Bayesian framework that extends our earlier approach to a multi-dimensional formulation. Our model incorporates distinct mathematical distributions that capture sampling bias patterns in tumour data, allowing the deconvolution to resist the effect of some confounders. This works presents the simulation of one source of sampling bias analysed with this new approach, together with a large scale test based on simulations. Moreover, we apply our model to understand subclonal deconvolution from a multi-region whole-genome colorectal cancer sample and from longitudinal whole-genome glioblastoma samples of 15 patients collected before and after treatment. This new deconvolution approach offers a better account of the effect of spatio-temporal tumour biases, allowing us to better elucidate complex clonal dynamics from multi-sample cancer sequencing data
DivNoise: A Data Collection for Source Identification on Diverse Camera Sensors
No full textIdentifying the acquisition source of media data is one of the most widely studied problems in multimedia forensics. A crucial aspect in this field is the availability of representative, diverse and up-to-date data corpora, so that the potential of existing and newly proposed techniques can be assessed in a reliable and reproducible manner. In this light, we present a novel dataset, named DivNoise, which encompasses both image and video data from a wide range of device cameras and collected in different environmental conditions. In particular, differently from existing databases, the dataset also includes data acquired from frontal cameras of mobile devices (smartphones and tablets) and from webcams, which are increasingly used tools to enable remote video communications in many application scenarios. The dataset is made publicly available to the research community, with the goal of supporting the development of novel source identification techniques. We perform an experimental evaluation on the DivNoise dataset through state-of-the-art algorithms, thus exposing preliminary yet intriguing empirical insights
Composing FOCoRe Hybrid Automata
No full textThis paper addresses questions regarding the decidability ofhybrid automata that may be built hierarchically as is the case in many exemplar systems, be it natural or engineered. Parallel composition canbe considered a fundamental tool in such costructions. Somewhat surprisingly, this operation does not always preseve the decidability of reachability problem i.e., even if we prove the decidability of reachability overcomponent automata, we cannot guarantee the decidability over theirparallel composition. Despite these limitations, this paper provides a re-duction for the reachability problem over parallel composition of first-order constant reset automata (FOCoRe) to the satisfiability of a particular linear Diophantine system. Moreover, since such satisfiability problem have been proved decidable for systems with semi-algebraic coefficients,this paper presents an interesting class of hybrid automata for which the reachability problem of parallel composition is decidable. The resulting hybrid automata appear in systems biological modeling, and hence could be applied when one is interested in understanding a complex biological system composed of many smaller self-organizing systems
Discrete Semantics for Hybrid Automata
Full text linkMany natural systems exhibit a hybrid behavior characterized by a set of continuous laws which are switched by discrete events. Such behaviors can be described in a very natural way by a class of automata called hybrid automata. Their evolution are represented by both dynamical systems on dense domains and discrete transitions. Once a real system is modeled in a such framework, one may want to analyze it by applying automatic techniques, such as Model Checking or Abstract Interpretation. Unfortunately, the discrete/continuous evolutions not only provide hybrid automata of great flexibility, but they are also at the root of many undecidability phenomena. This paper addresses issues regarding the decidability of the reachability problem for hybrid automata (i.e., "can the system reach a state a from a state b?") by proposing an "inaccurate" semantics. In particular, after observing that dense sets are often abstractions of real world domains, we suggest, especially in the context of biological simulation, to avoid the ability of distinguishing between values whose distance is less than a fixed ε. On the ground of the above considerations, we propose a new semantics for first-order formulæ which guarantees the decidability of reachability. We conclude providing a paradigmatic biological example showing that the new semantics mimics the real world behavior better than the precise one
- …
