waashk/dblp huggingface dataset:
processes of membrane systems with promoters and inhibitors. membrane systems (with promoters and inhibitors) are a computational model inspired by the way living cells are divided by membranes into compartments where chemical reactions may take place. we consider synchrony and asynchrony between executed reactions in the computations of such systems using petri nets and their processes as a formal behavioural model. we first discuss different definitions of individual computational steps, and show how they can be rendered within the petri net domain by assigning all transitions localities corresponding to the compartments, and using activator and inhibitor arcs. the non-sequential semantics of the resulting nets is formalised through processes based on occurrence nets augmented with additional information about localities and activator/inhibitor arcs. such processes provide a convenient tool for analysing synchrony and asynchrony in the executions of membrane systems and shed light on the causal relationships between the reactions taking place.
on the decidability and complexity of the structural congruence for beta-binders. beta-binders is a recent process calculus developed for modelling and simulating biological systems. as usual for process calculi, the semantic definition heavily relies on a structural congruence. the treatment of the structural congruence is essential for implementation. we present a subset of the calculus for which the structural congruence is decidable and a subset for which it is also efficiently solvable. the obtained results are a first step towards implementations.
a simple calculus for proteins and cells. the use of process calculi to represent biological systems has led to the design of different formalisms such as brane calculi and @k-calculus. both have proved to be useful to model different types of biological systems. as an attempt to unify the formalisms, we introduce the bio@k-calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. in bio@k-calculus, protein-protein interactions have to be at most binary and cell interactions have to fit with sort constraints. in this contribution we define the semantics of bio@k-calculus, analyse its properties, discuss the expressivity of the calculus by modelling two significant examples-a signalling pathway and a virus infection-and study an implementation in milner's @p-calculus.
computational self-assembly. the object of this paper is to probe the computational limits of an applied concurrent language called @k. this language describes how agents can bind and modify each other. it is meant as a syntactic medium to build, discuss and execute descriptions of cellular signalling pathways. however, it can be studied independently of its intended interpretation, and this is what we are doing here. specifically, we define a reduction of @k to a fragment where interactions can involve at most two agents at a time. the translation relies on an implicit causality analysis which permits escaping deadlocks. it incurs only a linear blow up in the number of rules. its correctness is spelt out in terms of the existence of a specific weak bisimulation and is proved in detail. to compensate for the binary restriction, one allows components to create unique names. when using acyclic rules, this additional facility of name creation is not needed and @k can be reduced to a binary form as is.
membrane systems with proteins embedded in membranes. membrane computing is a biologically inspired computational paradigm. motivated by brane calculi we investigate membrane systems which differ from conventional membrane systems by the following features: (1) biomolecules (proteins) can move through the regions of the systems, and can attach onto (and de-attach from) membranes, and (2) membranes can evolve depending on the attached molecules. the evolution of membranes is performed by using rules that are motivated by the operation of pinocytosis (the pino rule) and the operation of cellular dripping (the drip rule) that take place in living cells. we show that such membrane systems are computationally universal. we also show that if only the second feature is used then one can generate at least the family of parikh images of the languages generated by programmed grammars without appearance checking (which contains non-semilinear sets of vectors). if, moreover, the use of pino/drip rules is non-cooperative (i.e., not dependent on the proteins attached to membranes), then one generates a family of sets of vectors that is strictly included in the family of semilinear sets of vectors. we also consider a number of decision problems concerning reachability of configurations and boundness.
membrane computing and brane calculi. old, new, and future bridges. after a short discussion about similarities and dissimilarities of membrane computing and brane calculi, insisting mainly on some recent ideas of bridging the two areas of research, one recalls some details concerning certain classes of p systems based on brane calculi operations. several open problems are formulated in this context.
decision problems in membrane systems with peripheral proteins, transport and evolution. transport of substances and communication between compartments are fundamental biological processes, often mediated by the presence of complementary proteins attached to the surfaces of membranes. within compartments, substances are acted upon by local biochemical rules. inspired by this behaviour we present a model based on membrane systems, with objects attached to the sides of the membranes and floating objects that can be moved between the regions of the system. moreover, in each region there are evolution rules that rewrite the transported objects, mimicking chemical reactions. we investigate qualitative properties, like configuration reachability, in relation to the use of cooperative or non-cooperative evolution and transport rules and in the contexts of free- and maximal-parallel evolution.
elementary differences among jump classes. it is shown that th(h"1)1, where h"m is the upper semi-lattice of all high"m computably enumerable (c.e.) degrees for m>0, giving a first elementary difference among the highness hierarchies of the c.e. degrees.
semi-formal verification of the steady state behavior of mixed-signal circuits by sat-based property checking. in this article, a verification methodology for mixed-signal circuits is presented that can easily be integrated into industrial design flows. the proposed verification methodology is based on formal verification methods. a vhdl behavioral description of a mixed-signal circuit is transformed into a discrete model and then verified using well-established tools from formal digital verification. using the presented methodology, a much higher coverage of the functionality of a mixed-signal circuit can be achieved than with simulation based verification methods. the approach has already been successfully applied to industrial mixed-signal circuits.
embedding finite automata within regular expressions. regular expressions and their extensions have become a major component of industry-oriented specification languages such as ieee psl [ieee standard for property specification language (psl). ieee std 1850(tm)-2005]. the model checking procedure of regular expression based formulas, involves constructing an automaton which runs in parallel with the model. in this paper we re-examine the automata construction. we propose an algorithm that allows an intermediate representation mixing both regular expressions and automata. this representation can be thought of as plugging an automaton inside a regular expression, to replace an existing sub-expression. in order to be verified, the intermediate representation is then translated into another automaton, resulting in a set of automata running in parallel. a key feature of this algorithm is that the plug-in automaton is independent of the regular expression from which it originated, and thus can be used in several different properties. we demonstrate the usefulness of our method by providing a set of applications. we show how the use of our method allows modularity and flexibility of the automata construction, and can increase expressiveness when seres are mixed with ctl. we give two applications for which it significantly reduces the size of the automata built for formulas, thus reducing the overall run time of the model checking procedure.
on model checking multiple hybrid views. many applications, for instance the ms .net global assembly cache (gac), are naturally expressed as 3-valued models where an additional third truth value models uncertainty or under-specification. an example of under-specification is that a component in a gac may or may not have a main method. models described in this manner can then be analyzed to refute or verify properties about the concrete systems they intend to model. this approach to system validation traditionally considers only one model at a time, even though this model may evolve if subjected to analysis. many applications, however, benefit from or require the simultaneous consideration of multiple models of systems. we mention here requirements from different stake holders, and data drawn from federated databases. this paper therefore builds the mathematical foundations for property verification and refutation as applied to finitely many 3-valued models, where each model is endowed with states - possibly named by nominals, also known as hybrid constraints - labelled transitions, and atomic propositions. specifically, we show that deciding whether a finite set of models has a common concrete system (consistency) is typically in ptime, and that deciding whether a common concrete system satisfies a formula of the hybrid mu-calculus (satisfiability), and its dual (validity), are exptime-complete. we propose sound and efficient approximations of these exptime-complete checks by synthesizing and checking ''summary'' models. these approximations are optimal if all models are deterministic. finally, we point out that such optimality of summary models is unattainable whenever not all summarized models are deterministic.
a probabilistic alternative to regression suites. automated regression suites are essential in developing large applications, while maintaining reasonable quality and timetables. the main argument against the automation of regression suites, in addition to the cost of creation and maintenance, is the observation that if you run the same test many times, it becomes increasingly less likely to find bugs. to alleviate such problems, a new regression suite practice, using random test generators to create regression suites on-the-fly, is becoming more common. in this practice, instead of maintaining tests, we generate test suites on-the-fly by choosing several specifications and generating a number of tests from each specification. we describe techniques for optimizing random generated test suites. we first show how the set cover greedy algorithms, commonly used for selecting tests for regression suites, may be adapted to selecting specifications for randomly generated regression suites. we then introduce a new class of greedy algorithms, referred to as future-aware greedy algorithms. the algorithms are computationally efficient and generate more effective regression suites.
an automatic abstraction technique for verifying featured, parameterised systems. a general technique combining model checking and abstraction is presented that allows property based analysis of systems consisting of an arbitrary number of featured components. we show how parameterised systems can be specified in a guarded command form with constraints placed on variables which occur in guards. we prove that results that hold for a small number of components can be shown to scale up. we then show how featured systems can be specified in a similar way, by relaxing constraints on guards. the main result is a generalisation theorem for featured systems which we apply to two well known examples.
automatic generation of path conditions for concurrent timed systems. this paper presents an automatic method for calculating the path condition for programs with real time constraints. we model concurrent systems using timed transition systems and translate them into extended timed automata. then an acyclic extended timed automaton is constructed and the path condition is calculated backwards over it. this method can be used for semiautomatic verification of a unit of code in isolation, i.e., without providing the exact values of parameters with which it is called. it can also be used for test case generation for real-time systems. such a symbolic model checking algorithm was implemented previous in the pet system [e. gunter, d. peled, unit checking: symbolic model checking for a unit of code, verification: theory and practice 2003, essays dedicated to zohar manna on the occasion of his 64th birthday, lecture notes in computer science, vol. 2772, springer, 548-567] for untimed systems. our method can also be used for the automatic generation of test cases for unit testing. the current generalization of the calculation of path condition for the timed case turns out to be quite tricky, since not only the selected path contributes to the path condition, but also timing constraints of alternative choices in the code.
efficient sat-based bounded model checking for software verification. this paper discusses our methodology for formal analysis and automatic verification of software programs. it is applicable to a large subset of the c programming language that includes pointer arithmetic and bounded recursion. we consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. we perform this analysis via a translation to a boolean circuit representation based on modeling basic blocks. the program is then analyzed by a back-end sat-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program. the main contributions of this paper are as follows: (1) use of basic block-based unrollings with sat-based bounded model checking of software programs. this allows us to take advantage of sat-based learning inherent to the best performing bounded model checkers. (2) various heuristics customized for models automatically generated from software, allowing a more efficient sat-based analysis. (3) a prototype tool called f-soft has been implemented using our methodology. we present experimental results based on multiple case studies including a c-based implementation of a network protocol, and compare the performance gains using the proposed heuristics.
consistency of discrete bayesian learning. bayes' rule specifies how to obtain a posterior from a class of hypotheses endowed with a prior and the observed data. there are three fundamental ways to use this posterior for predicting the future: marginalization (integration over the hypotheses w.r.t. the posterior), map (taking the a posteriori most probable hypothesis), and stochastic model selection (selecting a hypothesis at random according to the posterior distribution). if the hypothesis class is countable, and contains the data generating distribution (this is termed the ''realizable case''), strong consistency theorems are known for the former two methods in a sequential prediction framework, asserting almost sure convergence of the predictions to the truth as well as loss bounds. we prove corresponding results for stochastic model selection, for both discrete and continuous observation spaces. as a main technical tool, we will use the concept of a potential: this quantity, which is always positive, measures the total possible amount of future prediction errors. precisely, in each time step, the expected potential decrease upper bounds the expected error. we introduce the entropy potential of a hypothesis class as its worst-case entropy, with regard to the true distribution. our results are proven within a general stochastic online prediction framework, that comprises both online classification and prediction of non-i.i.d. sequences.
leading strategies in competitive on-line prediction. we start from a simple asymptotic result for the problem of on-line regression with the quadratic loss function: the class of continuous limited-memory prediction strategies admits a ''leading prediction strategy'', which not only asymptotically performs at least as well as any continuous limited-memory strategy, but also satisfies the property that the excess loss of any continuous limited-memory strategy is determined by how closely it imitates the leading strategy. more specifically, for any class of prediction strategies constituting a reproducing kernel hilbert space, we construct a leading strategy, in the sense that the loss of any prediction strategy whose norm is not too large is determined by how closely it imitates the leading strategy. this result is extended to the loss functions given by bregman divergences and by strictly proper scoring rules.
finite relational structure models of topological spaces and maps. we define the notion of homotopy pushout in the category of binary reflexive relational structures and explore its basic properties. we construct finite models in this category, of spaces and maps in top with a view to developing systematic methods in this regard.
kernel methods for learning languages. this paper studies a novel paradigm for learning formal languages from positive and negative examples which consists of mapping strings to an appropriate high-dimensional feature space and learning a separating hyperplane in that space. such mappings can often be represented flexibly with string kernels, with the additional benefit of computational efficiency. the paradigm inspected can thus be viewed as that of using kernel methods for learning languages. we initiate the study of the linear separability of automata and languages by examining the rich class of piecewise-testable languages. we introduce a subsequence feature mapping to a hilbert space and prove that piecewise-testable languages are linearly separable in that space. the proof makes use of word combinatorial results relating to subsequences. we also show that the positive definite symmetric kernel associated to this embedding is a rational kernel and show that it can be computed in quadratic time using general-purpose weighted automata algorithms. our examination of the linear separability of piecewise-testable languages leads us to study the general problem of separability with other finite regular covers. we show that all languages linearly separable under a regular finite cover embedding, a generalization of the subsequence embedding we use, are regular. we give a general analysis of the use of support vector machines in combination with kernels to determine a separating hyperplane for languages and study the corresponding learning guarantees. our analysis includes several additional linear separability results in abstract settings and partial characterizations for the linear separability of the family of all regular languages.
topology in information theory in topology. we prove that timed capacity in information theory is a euclidean continuous function of noise. this is a result based on topological methods that benefits work in information theory. then we show that binary timing capacity is a measure of distance which yields the euclidean topology on the unit interval, despite the fact that it does not satisfy the triangle inequality. this is a result based on information theoretic methods that benefits topology. these results have important applications in an area known as information hiding, in the study of quantum communication and in domain theory. they appear to raise fundamental questions about the nature of distance itself.
computational complexity of determining which statements about causality hold in different space-time models. causality is one of the most fundamental notions of physics. it is therefore important to be able to decide which statements about causality are correct in different models of space-time. in this paper, we analyze the computational complexity of the corresponding decision problems. in particular, we show that: *for minkowski space-time, the decision problem is as difficult as tarski's decision problem for elementary geometry, while *for a natural model of primordial space-time, the corresponding decision problem is of the lowest possible complexity among all possible space-time models.
causal set topology. the causal set theory (cst) approach to quantum gravity is motivated by the observation that, associated with any causal spacetime (m,g) is a poset (m,@?), with the order relation @? corresponding to the spacetime causal relation. spacetime in cst is assumed to have a fundamental atomicity or discreteness, and is replaced by a locally finite poset, the causal set. in order to obtain a well defined continuum approximation, the causal set must possess the requisite intrinsic topological and geometric properties that characterise a continuum spacetime in the large. the study of causal set topology is thus dictated by the nature of the continuum approximation. we review the status of causal set topology and present some new results relating poset and spacetime topologies. the hope is that in the process, some of the ideas and questions arising from cst will be made accessible to the larger community of computer scientists and mathematicians working on posets.
unsupervised slow subspace-learning from stationary processes. we propose a method of unsupervised learning from stationary, vector-valued processes. a projection to a low-dimensional subspace is selected on the basis of an objective function which rewards data-variance and penalizes the variance of the velocity vector, thus exploiting the short-time dependencies of the process. we prove bounds on the estimation error of the objective in terms of the @b-mixing coefficients of the process. it is also shown that maximizing the objective minimizes an error bound for simple classification algorithms on a generic class of learning tasks. experiments with image recognition demonstrate the algorithms ability to learn geometrically invariant feature maps.
lawson topology of the space of formal balls and the hyperbolic topology. let (x,d) be a metric space and bx=xxr denote the partially ordered set of (generalized) formal balls in x. we investigate the topological structures of bx, in particular the relations between the lawson topology and the product topology. we show that the lawson topology coincides with the product topology if (x,d) is a totally bounded metric space, and show examples of spaces for which the two topologies do not coincide in the spaces of their formal balls. then, we introduce a hyperbolic topology, which is a topology defined on a metric space other than the metric topology. we show that the hyperbolic topology and the metric topology coincide on x if and only if the lawson topology and the product topology coincide on bx.