-
Article
On Induction Principles for Partial Orders
Various forms of mathematical induction (induction for natural numbers, transfinite induction, structural induction, well-founded induction, Noetherian induction, etc.) are applicable to domains with some kind...
-
Chapter and Conference Paper
On Induction Principles for Diamond-Free Partial Orders
We propose a formulation of an induction principle for diamond-free partial orders, which can be considered as a generalization of one of the variants of the real induction principle. This principle may be use...
-
Chapter and Conference Paper
Expressibility in the Kleene Algebra of Partial Predicates with the Complement Composition
In the paper we investigate the expressibility of partial predicates in the Kleene algebra extended with the composition of predicate complement and give a necessary and sufficient condition of this expressibi...
-
Chapter and Conference Paper
Inference Rules for the Partial Floyd-Hoare Logic Based on Composition of Predicate Complement
Classical Floyd-Hoare logic is sound when total pre- and post-conditions are considered. In the case of partial conditions (predicates) the logic becomes unsound. This situation may be corrected by introducing...
-
Chapter and Conference Paper
On Formalization of Semantics of Real-Time and Cyber-Physical Systems
In the article we describe theoretical foundations of a framework for formalizing semantics of real-time and cyber-physical systems in interactive theorem proving environments. The framework is based on viewi...
-
Chapter and Conference Paper
Formalization of the Nominative Algorithmic Algebra in Mizar
We describe a formalization of the nominative algorithmic algebra in the Mizar proof assistant. This algebra is a generalization of Glushkov algorithmic algebras which is well suited for representing semantic...
-
Chapter and Conference Paper
Extended Floyd-Hoare Logic over Relational Nominative Data
The classical Floyd-Hoare logic is defined for the case of total pre- and postconditions and partial programs (i.e. programs can be undefined on some input data, but conditions must be defined on all data). In...
-
Chapter and Conference Paper
On Local Characterization of Global Timed Bisimulation for Abstract Continuous-Time Systems
We consider two notions of timed bisimulation on states of continuous-time dynamical systems: global and local timed bisimulation. By analogy with the notion of a bisimulation relation on states of a labeled t...
-
Chapter and Conference Paper
On Representations of Abstract Systems with Partial Inputs and Outputs
We consider a class of mathematical models called blocks which generalize some input-output models which appear in mathematical systems theory, control theory, signal processing. A block maps partial functions...
-
Chapter and Conference Paper
On a Decidable Formal Theory for Abstract Continuous-Time Dynamical Systems
We propose a decidable formal theory which describes high-level properties of abstract continuous-time dynamical systems called Nondeterministic Complete Markovian Systems (NCMS). NCMS is a rather general clas...
-
Chapter and Conference Paper
On Algebraic Properties of Nominative Data and Functions
In the chapter basic properties of nominative data and functions over nominative data (nominative functions) are investigated from the perspective of abstract algebra. A set of all nominative data over arbitra...
-
Chapter and Conference Paper
On Existence of Total Input-Output Pairs of Abstract Time Systems
We consider a class of abstract mathematical models called blocks which generalize some input-output system models which are frequently used in system theory, cybernetics, control theory, signal processing. A ...
-
Chapter and Conference Paper
A Criterion for Existence of Global-in-Time Trajectories of Non-deterministic Markovian Systems
We consider the following question: given a continuous-time non-deterministic (not necessarily time-invariant) dynamical system, is it true that for each initial condition there exists a global-in-time traject...
