Feasibility of finite and infinite paths in data dependent programs

This paper considers the feasibility of finite and infinite paths in programs in two simple programming languages. The language LBASE allows to express the dependencies of real time systems on integer data, the language LTIM can model quantitative timing constraints in r.t.s. specifications. It is proven that the problem of whether a given LBASE or LTIM program has an infinite feasible path (i.e. whether it can exhibit an infinite behaviour) is decidable. The possibilities to characterise the sets of all feasible finite and infinite paths in LBASE and LTIM programs are also discussed. The infinite feasible path existence problem is proven decidable also for the language LTIBA which has both…

General decidability theorems for infinite-state systems

Over the last few years there has been an increasing research effort directed towards the automatic verification of infinite state systems. This paper is concerned with identifying general mathematical structures which can serve as sufficient conditions for achieving decidability. We present decidability results for a class of systems (called well-structured systems), which consist of a finite control part operating on an infinite data domain. The results assume that the data domain is equipped with a well-ordered and well-founded preorder such that the transition relation is "monotonic" (is a simulation) with respect to the preorder. We show that the following properties are decidable for …

Pini Language and PiniTree Ontology Editor: Annotation and Verbalisation for Atomised Journalism

We present a new ontology language Pini and the PiniTree ontology editor supporting it. Despite Pini language bearing lot of similarities with RDF, UML class diagrams, Property Graphs and their frontends like Google Knowledge Graph and Protege, it is a more expressive language enabling FrameNet-style natural language annotation for Atomised journalism use case.

Domain-Specific OWL Ontology Visualization with OWLGrEd

The OWLGrEd ontology editor allows graphical visualization and authoring of OWL 2.0 ontologies using a compact yet intuitive presentation that combines UML class diagram notation with textual Manchester syntax for expressions. We present an extension mechanism for OWLGrEd that allows adding custom information areas, rules and visual effects to the ontology presentation thus enabling domain specific OWL ontology visualizations. The usage of OWLGrEd and its extensions is demonstrated on ontology engineering examples involving custom annotation visualizations, advanced UML class dia-gram constructs and integrity constraints in semantic database schema design.

CTR: A calculus of timed refinement

This paper presents CTR — a process algebraic framework for loose specification of time quantity sensitive operational behaviour of reactive systems. CTR terms are provided both with operational and specification semantics (via the notion of specification refinement). Besides the intuitive justification of appropriateness of the refinement notion, a preservation theorem is proved for a timed variant of Hennessy-Milner logic. A comparison of CTR with the related formalism of Timed Modal Specifications, and with the timed process calculi TCCS due to Wang is given. Some pragmatics of the application of CTR is sketched on a critical resource access example.

Deciding properties of integral relational automata

This paper investigates automated model checking possibilities for CTL* formulae over infinite transition systems represented by relational automata (RA). The general model checking problem for CTL* formulae over RA is shown undecidable, the undecidability being observed already on the class of Restricted CTL formulae. The decidability result, however, is obtained for another substantial subset of the logic, called A-CTL*+, which includes all ”linear time” formulae.

Ontology-Based Information System

We describe a novel way for creating information systems based on ontologies. The described solution is aimed at domain experts who would benefit from being able to quickly prototype fully-functional, web-based information system for data input, editing and analysis. The systems backbone is SPARQL 1.1 endpoint that enables organization users to view and edit the data, while outside users can get read-only access to the endpoint. The system prototype is implemented and successfully tested with Latvian medical data ontology with 60 classes and imported 5 000 000 data-level triples.

Dynamics of gene regulatory networks and their dependence on network topology and quantitative parameters – the case of phage λ

Background Gene regulatory networks can be modelled in various ways depending on the level of detail required and biological questions addressed. One of the earliest formalisms used for modeling is a Boolean network, although these models cannot describe most temporal aspects of a biological system. Differential equation models have also been used to model gene regulatory networks, but these frameworks tend to be too detailed for large models and many quantitative parameters might not be deducible in practice. Hybrid models bridge the gap between these two model classes – these are useful when concentration changes are important while the information about precise concentrations and binding…

Efficient learning of regular expressions from good examples

We consider the problem of restoring regular expressions from expressive examples. We define the class of unambiguous regular expressions, the notion of the union number of an expression showing how many union operations can occur directly under any single iteration, and the notion of an expressive example. We present a polynomial time algorithm which tries to restore an unambiguous regular expression from one expressive example. We prove that if the union number of the expression is 0 or 1 and the example is long enough, then the algorithm correctly restores the original expression from one good example. The proof relies on original investigations in theory of covering symbol sequences (wo…

Automatic construction of test sets: Theoretical approach

We consider the problem of automatic construction of complete test set (CTS) from program text. The completeness criterion adopted is C1, i.e., it is necessary to execute all feasible branches of program at least once on the tests of CTS. A simple programming language is introduced with the property that the values used in conditional statements are not arithmetically deformed. For this language the CTS problem is proved to be algorithmically solvable and CTS construction algorithm is obtained. Some generalizations of this language containing counters, stacks or arrays are considered where the CTS problem remains solvable. In conclusion the applications of the obtained results to CTS constr…

Graph-based characterisations of cell types and functionally related modules in promoter capture Hi-C Data

Grammar based content completion method using Lua LPeg.re module

A grammar based content completion method for Lua programming language and its LPeg.re module environment is described in this paper. The use of our method is not demanding in computing resources, as well as it is easy to add the content completion functionality to any target language grammar. We report on the application of our method for OWL Manchester syntax expression grammar, as well as custom database-to-ontology mapping language.

Simulation is decidable for one-counter nets

We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of sim…

From Databases to Ontologies

This chapter introduces the UML profile for OWL as an essential instrument for bridging the gap between the legacy relational databases and OWL ontologies. We address one of the long-standing relational database design problems where initial conceptual model (a semantically clear domain conceptualization ontology) gets “lost” during conversion into the normalized database schema. The problem is that such “loss” makes database inaccessible for direct query by domain experts familiar with the conceptual model only. This problem can be avoided by exporting the database into RDF according to the original conceptual model (OWL ontology) and formulating semantically clear queries in SPARQL over t…

Decidability of bisimulation equivalences for parallel timer processes

In this paper an abstract model of parallel timer processes (PTPs), allowing specification of temporal quantitative constraints on the behaviour of real time systems, is introduced. The parallel timer processes are defined in a dense time domain and are able to model both concurrent (with delay intervals overlapping on the time axis) and infinite behaviour. Both the strong and weak (abstracted from internal actions) bisimulation equivalence problems for PTPs are proved decidable. It is proved also that, if one provides the PTP model additionally with memory cells for moving timer value information along the time axis, the bisimulation equivalence (and even the vertex reachability) problems …

Additional file 1 of Dynamics of gene regulatory networks and their dependence on network topology and quantitative parameters – the case of phage λ

Software package implementing our proposed method of attractor analysis. It contains source files, user manual and the phage λ model described in this manuscript. Following subsections describe files from the package. ModelDescription.txt: Definition of the phage λ model that is analysed within this paper. ModelConstraints.txt: File that specifies partial constraints for the orderings of binding site affinities. Here, the constraints are applicable to our phage λ model. HSM_graph_analysis.cpp: The main component of the software that identifies all feasible states of a system. HSM_graph_analysis.h: The second component of the software for graph analysis. It is a C++ header file which contain…