# Automation of Presentation Record Production Based on Rich-Media Technology Using SNT Petri Nets Theory

Authors: Ivo Martiník
Journal: The Scientific World Journal
 (2015)

---

## Abstract

Rich-media describes
a broad range of digital interactive media that
is increasingly used in the Internet and also in
the support of education. Last year, a special
pilot audiovisual lecture room was built as a
part of the MERLINGO (MEdia-rich
Repository of LearnING Objects) project
solution. It contains all the elements of the
modern lecture room determined for the
implementation of presentation recordings based
on the rich-media technologies and their
publication online or on-demand featuring the
access of all its elements in the automated mode
including automatic editing. Property-preserving
Petri net process algebras (PPPA) were designed
for the specification and verification of the
Petri net processes. PPPA does not need to
verify the composition of the Petri net
processes because all their algebraic operators
preserve the specified set of the properties.
These original PPPA are significantly
generalized for the newly introduced class of
the SNT Petri process and agent nets in this
paper. The PLACE-SUBST and ASYNC-PROC
algebraic operators are defined for this class
of Petri nets and their chosen properties are
proved. The SNT Petri process and agent nets
theory were significantly applied at the design,
verification, and implementation of the
programming system ensuring the pilot
audiovisual lecture room
functionality.


---

## Body

## 1. Introduction

The term rich-media describes a broad range of digital interactive media, through which it is possible to share and transfer information and communicate in various ways. Moreover, rich-media enable interactivity, that is, bidirectional communication. The characteristic feature of the rich-media technologies is their accessibility online or on-demand, followed by the support of the dynamics of changes. An example can be online streaming video reporting, which is updated during broadcast, or a record of presentation placed on a website jointly with the synchronized slide show, which the user can interactively work with. Currently, there are several theories dealing with various aspects of the rich-media implementation, such asMedia Richness Theory [1],Media Naturalness Theory [2], andSocial Presence Theory [3].The issue of majority aspects in implementing rich-media technologies at selected universities in the Czech Republic is dealt with in the MERLINGO project (MEdia-rich Repository of LearnING Objects) [4]. One of the key objectives of this project last year was the implementation of the cutting edge rich-media technologies in order to build a specialized audiovisual lecture room containing all the elements of a modern lecture room determined for the implementation of presentation recordings and their publication online or on-demand featuring the integrated ergonomic and intuitive control and access in the automated mode of all its elements including automatic editing. Next objective was to provide a possibility of parallel sharing and feedback of lectures presented in the lecture room outfitted as such in real time even at other audiovisual auditoriums while providing the services of the central repository of educational objects MERLINGO and the possibility of their adaptation for the students with special needs. The implementation of those functionalities significantly contributed in decrease of costs required for the operation of high-capacity lecture halls including reduction of time and space demands mainly required for teaching subjects determined for large groups of students. Currently, the operation of the central repository MERLINGO dramatically simplifies the implementation of the new revolutionary technologiesEduArt [5] andMediaInTouch [6], featuring unique characteristics in this area complying with demanding requirements of teachers in the availability and quality of presentation recordings.Petri nets [7–14] represent a popular formalism connecting advantages of the graphic representation of a modeled system with the possibilities of its simulation and the formal analyzability. Property-preserving Petri net process algebras (PPPA) [15] were originally designed for the specification and verification of manufacturing systems. PPPA also follows many ideas that can be originally seen in the class of workflow nets [16]. The elements of PPPA are the Petri net processes, ordinary connected Petri nets with a unique entry place, a unique exit place, and a set of places for handling resource sharing with their initial marking allowed. Among other features, PPPA does not need to verify composite components because all its operators preserve many properties. Hence, if the primitive modules satisfy the desirable properties, each of the composite components, including the system itself, also satisfies these properties.PPPA has five types of operators: extensions, compositions, refinements, reductions, and place-merging. All the operators can preserve about twenty properties (some under additional conditions), such as liveliness, boundedness, reversibility, traps, siphons, and proper termination.The main goals of this paper are to generalize PPPA for the newly introduced class of the SNT Petri process and agent nets (SNTPAN) and to define the new SNTPAN operators called PLACE-SUBST (PLACE-SUBSTitution) and ASYNC-PROC (ASYNChronous-PROCessing) with the property of the SNTPAN soundness preservation. This class of SNTPANs with the support of the PLACE-SUBST and ASYNC-PROC operators that preserve the soundness property during the SNTPAN components composition process has been applied at the design, verification, simulation, and implementation phases of the software support of the audiovisual lecture room enabling automated recordings of the presentations including automated editing.


## 2. Materials and Methods

### 2.1. SNT Petri Process and Agent Nets and Their Properties

LetN denote the set of all natural numbers, N0 the set of all nonnegative integer numbers, ∅ the empty set, ⌐ the logical negation operator, A the cardinality of the given set A, where N=ℵ0, P(A) the family of all the subsets of a given set A, and IDENT the set of all identifiers over a certain alphabet.Multiset
M over a nonempty set S is a function m:S→N0. The nonnegative number m(a)∈N0, where a∈S, denotes the number of occurrences of the element a in the multiset m. The multiset m is usually represented by the formal sum ∑a∈Sma′a. SMS denotes the set of all nonempty multisets over the set S and SMSE denotes the set of all multisets over the set S.LetA be a nonempty set. By the (nonempty finite)sequenceσ over the set A a function σ can be understood, σ:{1,2,…,n}→A, where n∈N. The function ε:∅→A is called theempty sequence over the set A. The sequence σ:{1,2,…,n}→A is usually represented by the notation σ=a1,a2,…,an or σ=a1a2⋯an of the elements of the set A, where ai=σ(i) for 1≤i≤n. Empty sequence ε:∅→A over the set A is usually represented by the notation ε=. The set of all finite nonempty sequences over the set A is denoted by the notation ASQ and the set of allfinite (and possible empty) sequences over the set A by the notation ASQE. Thelength of the sequenceσ=a1,a2,…,an, where n∈N, is equal to the natural number n and the length of the empty sequence ε is equal to the number 0. The length of the sequence σ is represented by the notation length(σ). The function elem:ASQE→P(A), such that elem(σ)={a∣∃i:a=σ(i),  where1≤i≤length(σ)}, elem(ε)=∅, assigns to each sequence σ∈ASQE the set of all of itselements.LetA={a1,a2,…,an}, where n∈N, be a finite nonempty set.VectorV is a function V:A→N0. We will denote a vector V by the statement V=(V(1),V(2),…,V(n)).LetV={(V(1),V(2),…,V(n))∣V(i)∈N0for1≤i≤n} and W={(W(1),W(2),…,W(m))∣W(j)∈N0for1≤j≤m}. Then(1)
V
⊗
W
=
V
1
,
…
,
V
n
,
W
1
,
…
,
W
m
∣
V
i
∈
N
0
for
1
≤
i
≤
n
,
W
j
∈
N
0
for
1
≤
j
≤
m
,
i
f
V
≠
∅
∧
W
≠
∅
,
=
V
,
if
V
≠
∅
∧
W
=
∅
,
=
W
,
if
V
=
∅
∧
W
≠
∅
,
=
∅
,
i
f
V
=
∅
∧
W
=
∅
.It is clear that the operation ⊗ is associative (i.e., (V⊗W)⊗U=V⊗(W⊗U)).Asemigroup(S,⚪) is a set S together with an associative binary operation ⚪:S×S→S. Amonoid(M,⚪,u) is a semigroup (M,⚪) with an element u∈M such that ∀x∈M:u⚪x=x=x⚪u.Anet is an ordered triple NET=(P,T,A), where(i)
Pis a finite nonempty set ofplaces,(ii)
T is a finite set oftransitions, P∩T=∅,(iii)
A is a finite set ofarcs, A⊆(P×T)∪(T×P).A given net is then described with a bipartite graph containing a finite nonempty setP of places used for expressing conditions of a modeled system (we usually use circles for their representation), a finite set T of transitions describing changes in the modeled system (we usually draw them in the form of rectangles) and a finite set A of arcs being principally oriented while connecting a place with a transition or a transition with a place and we usually draw them as lines with arrows. We say then a net (P,T,A) isconnected iff it is not composed of two or more disjoint and nonempty nets.Some commonly used notations for the nets are•y={x∣(x,y)∈A} for thepreset and y•={x∣(y,x)∈A} for thepostset of a net element y (i.e., place or transition).ASNT net (single-number tokens net) is an ordered 5-tuple SNTN=(P,T,A,AF,TP), where(i)
(P,T,A) is a connected net, ∀p∈P:›p⊆›p,(ii)
AF is the arc function, AF:(P×T)∪(T×P)→N0SQE, AF(x,y)∈N0SQ iff (x,y)∈A, AFx,y= iff (x,y)∉A, where x,y∈P∪T,∀t∈T∃k∈N∀p∈(•t∪t•): length(AF(p,t))=length(AF(t,p))=k,(iii)
TP is the transition priority function, TP:T→N.The arc functionAF of a given SNT net assigns each arc with a (nonempty) sequence of the nonnegative integer numbers expressing a removed or added token from or to the place associated with that arc when executing a particular transition. There must be the only one length k(k∈N) of all the values of the arc function AF (i.e., for the sequences of nonnegative integer numbers) for the given transition t and all of its associated input and output arcs. Transition priority function TP of a given SNT net assigns with each transition the natural number value expressing its priority (transition priority function has the default value of 1 if it is not explicitly indicated in the SNT net diagram).LetSNTN=(P,T,A,AF,TP) be a SNT net and p∈P a place. We will define the sets ›p∈P(N) of theplace input tokens and p›∈P(N) of theplace output tokens by the following way:›p=def{elem(AF(t,p))∣t∈•p}, if •p≠∅,›p=defp›, if (•p=∅)∧(p•≠∅),›p=defN, if (•p=∅)∧(p•=∅),p›=def{elem(AF(p,t))∣t∈p•}, if p•≠∅,p›=def›p, if (p•=∅)∧(•p≠∅),p›=defN, if (•p=∅)∧(p•=∅).Then the condition›p⊆›p must be true for all the places p of the given SNT netSNTN.Marking
M of the SNT netSNTN is a mapping M:P→N0MSE such that ∀p∈P∀e∈M(p):e∈p› (i.e., every token e represents the chosen single nonnegative integer number and every token e that is associated with the place p in the marking M must be an element of the set p› of the place output tokens). Marking M of a given SNT net then assigns each place with the multiset over the set N0 of all the nonnegative integer numbers and we use the form of m for the single token representation in the net diagrams, where m∈N0. Marking M of the SNT net then expresses the current status of a process that is modeled by the given SNT net. If P={P1,P2,…,Pn}, where n∈N, then marking M of given SNT net can be written as a P-vector M=(M(P1),M(P2),…,M(Pn)).ASNT Petri net is an ordered couple SNTPN=(SNTN,M0), where SNTN=(P,T,A,AF,TP) is a SNT net and M0:P→N0MSE is an initial marking of the netSNTN. We will then also denote a SNT Petri net by an ordered 6-tuple SNTPN=(P,T,A,AF,TP,M0).Transitiont∈T isenabled in the marking M of the SNT Petri netSNTPN if ∃ind∈N∀p∈•t∃e∈M(p):e=AF(p,t)(ind) and we denote that fact symbolically in the form of t enM.Firing of the transitiont∈T results in changing the marking M into the marking M′, where ∀p∈P:M′p=Mp∖AFp,tind∪AFt,pind, that is, denoted by MtM′. Marking Mn+1 isreachable from the marking M1 iff there exists a finite sequence σ=t1t2⋯tn of the transitions, where t1,t2,…,tn∈T, n∈N, such that M1t1M2t2M3⋯MntnMn+1. The set of all the markings reachable from the marking M will be denoted by the symbol M. The set of all finite and infinite transition sequences that are reachable from the marking M will be denoted by the symbol [M⟫; that is, M=t1t2⋯tn∣∃Mn+1∈M:Mt1t2⋯tnMn+1,n∈N.Figure1 illustrates the SNT Petri net N1=(P,T,A,AF,TP,M0), where(i)
P={P1,P2,P3,P4},(ii)
T={T1},(iii)
A={(P1,T1),(P2,T1),(T1,P3),(T1,P4)},(iv)
AF={((P1,T1),2,1),((P2,T1),2,3),((T1,P3),1,2),((T1,P4),1,1)},(v)
TP={(T1,1)},(vi)
M0=3′1,1′3,1′2,∅.Figure 1
Firing of transition in SNT Petri netN1.It can be seen that∀t∈T∃k∈N∀p∈(•t∪t•): length(AF(p,t))=length(AF(t,p))=k for the net N1, because for the only one transition T1∈T∃2∈N∀p∈(•T1∪T1•): length(AF(p,t))=length(AF(t,p))=2; that is, for any given transition t∈T and for all its input arcs (p,t) and all its output arcs (t,p) must be all the values of the arc functions AF(p,t) and AF(t,p) the sequences with the equal length k.We can also determine thatP1›={1,2} (because P1•≠∅ and P1›=  {elem(AF(P1,T1))}={1,2}), ›P1={1,2} (because (•P1=∅)∧(P1•≠∅), ›P1=P1›), P2›={2,3}=›P2,  P3›={1,2}=›P3, and P4›=1=›P4. We can also verify that the condition ∀p∈P∀e∈M0(p):e∈p› is fully satisfied for the net N1.Transition T1 is enabled in the markingM0 of the SNT Petri net N1 because ∃ind∈N∀p  ∈  •T1∃e∈M(p):e=AF(p,T1)(ind), where ind=2, •T1={P1,P2}, AF(P1,T1)(2)=1∈2′1  +  1′4 =  M0(P1), and AF(P2,T1)(2)=3∈1′3=M0(P2). Firing of the transition T1 results in changing of the net marking M0 into the marking M1, M0T1M1, where M1=(1′1+1′4,∅,1′2+1′5,1′1), because we will remove the token 1 from the place P1 and the token 3 from the place P2 and then we will add the token 2 (i.e., AF(T1,P3)(2)) into the place P3 and the token 1 (i.e., AF(T1,P4)(2)) into the place P4 according to the firing of the transition general rule.When enabling individual transitions of a given SNT Petri net so calledconflicts can originate in its certain markings (or conflict transitions). At the enabling of transitions t1 and t2 of the given SNT Petri net in its marking M, where t1, t2∈T, the conflict occurs, if ((•t1∩•t2≠∅)∧(t1enM)  ∧  (t2enM)∧⌐({t1,t2}enM)). The term of the conflict transitions can be obviously easily generalized for the case of the finite set t1,t2,…,tn(n∈N) of transitions of a given SNT Petri net.A typical example of conflict transitions in the particular marking of the SNT Petri netN2 is shown in Figure 2. The transitions T1 and T2 have the common input place P1; both are enabled but not enabled in parallel. When solving such transitions conflicts we will therefore follow the rule which determines, informally said, from the set of conflict transitions the one which will be enabled, whose value of the transition priority function TP is the highest. If such transition from the set of conflict transitions does not exist, the given conflict would have to be solved by other means. Our studied example will be then on the basis of that rule the transition T2 enabled (because TP(T1)=1 and TP(T2)=2).Figure 2
Conflict transitions in SNT Petri netN2.ASNT process net (PN) is an ordered 9-tuple PN=(P,T,A,AF,TP,RP,IP,OP,RMs), where(i)
(P,T,A,AF,TP) is aconnected SNT net,(ii)
RP is a finite set ofresource places, RP⊂P,(iii)
theinput placeIP is the only one place IP∈(P∖RP) such that •IP=∅,(iv)
theoutput placeOP is the only one place OP∈(P∖RP) such that OP•=∅,(v)
RMs is the set of all the allowedresource static markings (see below).The finite set of the resource placesRP is used for expressing the conditions of a modeled system containing some initial resources and we use circles with the double line for their representation. The input place IP is the only one place from the set P∖RP of the nonresource places that has no input transition and similarly the output place OP is the only one place from the set P∖RP of the nonresource places of the SNT process net that has no output transition. The class of all the SNT process nets will be denoted by the symbol PNET.Marking
M of the SNT process net PN is again a mapping M:P→N0MSE such that ∀p∈P∀e∈M(p):e∈p›. If RP={R1,R2,…,Rm}, where m∈N, P∖RP={IP,P1,P2,…,Pn,OP}, where n∈N, then the marking M can be written as a P-vector M=(M(IP),M(P1),M(P2),…,M(Pn),M(R1),  M(R2),…,M(Rm),M(OP)).Static marking
M
s of the SNT process net PN is a marking Ms such that ∀p∉RP:Ms(p)=∅; ∀t∈T:⌐(tenMs); that is, informally said, in the static marking Ms the tokens are allowed in the chosen resource places only and no transition is enabled in this static marking Ms. Static marking Ms of the SNT process net PN can then be written as a P-vector Ms=(∅,∅,∅,…,∅,Ms(R1),Ms(R2),…,Ms(Rm),∅). The set of all the allowed static markings Ms of the SNT process net PN we will denote by the symbol Ms.IfMs is the given static marking of the SNT process net PN, then by the symbol RMs we denote theresource static marking associated with the static marking Ms, that is, the function RMs:RP→N0MSE, where ∀p∈RP:RMs(p)=Ms(p) (i.e., informally said, resource static marking RMs associated with the static marking Ms of the SNT process net PN is the vector containing only the resource places markings of the static marking Ms and the static marking Ms of all the remaining places of the net PN is then equal to the empty set ∅). If RP={R1,R2,…,Rm}, where m∈N, then the resource static marking RMs of the SNT process net PN can be written as a RP vector RMs=(RMs(R1),RMs(R2),…,RMs(Rm)). The set of all the allowed resource static markings RMs associated with the set Ms of all allowed static markings Ms of the SNT process net PN will be denoted by the symbol RMs.Input marking
M
i of the SNT process net PN is a marking Mi such that Mi(IP)≠∅, Mi(OP)=∅, ∃Ms∈Ms∀p∈(P∖{IP,OP}):Mi(p)=Ms(p); that is, informally said, in the input marking Mi the input place IP must contain at least one token, the output place OP must not contain any token, and the marking Mi of the remaining places corresponds with the chosen static marking Ms from the set of all the allowed static markings Ms. We will denote this chosen static marking Ms∈Ms associated with the given input marking Mi by the symbol Msi. Input marking Mi of the process net PN can then be written as a P-vector Mi=(Mi(IP),∅,∅,…,∅,Msi(R1),Msi(R2),…,Msi(Rm),∅).Output (exit) marking
M
x reachable from the input marking Mi of the SNT process net PN is a marking Mx such that Mx(IP)=∅, Mx∈Mi, Mx(OP)=Mi(IP), and ∃Ms′∈Ms∀p∈(P∖{IP,OP}):Mx(p)  =  Ms′(p); that is, informally said, in the output marking Mx the input place IP must not contain any token, the output marking Mx is reachable from the input marking Mi, the output place OP must contain the same number of tokens in the output marking Mx as the input place IP in the input marking Mi and the markings of the remaining places correspond with the chosen static marking Ms′ from the set of allowed static markings Ms. We will denote this chosen static marking Ms′∈Ms associated with the given output marking Mx by the symbol Ms′x. Output marking Mx of the SNT process net PN can then be written as a P-vector Mx=(∅,∅,∅,…,∅,Ms′x(R1),Ms′x(R2),…,Ms′x(Rm),Mx(OP)). The set of all the output markings Mx that are reachable from the input marking Mi of the SNT process net PN will be denoted by the symbol Mix.Figure3 illustrates the SNT process net N3, where RP={R1} is the only one resource place of the net, IP is the input place IP, OP is the output place OP, and the set RMs of all its allowed resource static markings RMs={(1′1)}, in its static Ms, input Mi, and output Mx markings (note the resource place R1 with the initial token in the static marking Ms) where no transition must be enabled in (any) static marking Ms.Figure 3
Static, input, and output markings of the SNT process netN3.ASNT process Petri net is an ordered couple PPN=(PN,Mi), where PN=(P,T,A,AF,TP,RP,IP,OP,RMs) is a SNT process net and Mi is an input marking of the PN. We will then also denote a SNT process Petri net by an ordered 10-tuple PPN=(P,T,A,AF,TP,RP,IP,OP,RMs,Mi).ASNT agent net (AN) is an ordered 10-tuple AN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT), where(i)
(P,T,A,AF,TP) is aconnected SNT net,(ii)
RP is a finite set ofresource places, RP⊂P,(iii)
theinput placeIP is the only one place IP∈(P∖RP) such that •IP=∅,(iv)
theoutput placeOP is the selected place OP∈(P∖RP) such that OP•={OT},(v)
RMs is the set of all the allowedresource static markings,(vi)
theoutput transitionOT is the selected transition OT∈T such that •OT={OP}, TP(OT)=1.The concept of the SNT agent net such extends the concept of the SNT process net. So, informally said, the output placeOP is the selected place of the SNT agent net that has the single output transition OT and the output transition OT is the selected transition of the SNT agent net that has the single input place OP; it has no one output place and its transition priority function TP value is always the natural number 1. The meanings of the marking M, the static marking Ms, the input marking Mi, and the output marking Mx of the SNT agent net AN are the same as in the case of the SNT process net PN. The class of all the SNT agent nets will be denoted by the symbol ANET.Figure4 illustrates the SNT agent net N3, where RP={R1} is the only one resource place, IP is the input place IP, OP is the output place OP, OT is the output transition OT, and the set RMs of all its allowed resource static markings RMs={(1′1)}, in its input marking Mi.Figure 4
SNT agent netN4.LetAN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT) be a SNT agent net. The SNT process net AN_ associated with the SNT agent netAN is the 9-tuple AN_=(P_,T_,A_,AF_,TP_,RP_,IP_,OP_,RM_s_), where P_=P, T_=T∖{OT}, A_=A∖{(OP,OT)}, AF_=AF∖{((OP,OT),k)∣k∈N}, TP_=TP∖{(OT,1)}, RP_=RP, IP_=IP, OP_=OP, and RM_s_=RMs.ASNT agent Petri net is an ordered couple APN=(AN,Mi), where AN=(P,T,A,AF,TP,RP,IP,OP,   RMs,OT) is a SNT agent net and Mi is an input marking of the AN. We will then also denote a SNT agent Petri net by an ordered 11-tuple APN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT,Mi). A SNT process Petri net APN_=(AN_,Mi) is associated with the SNT agent Petri net APN=(AN,Mi).LetPPN=(P,T,A,AF,TP,RP,IP,OP,RMs,Mi) be a SNT process Petri net. A place p∈P is said to be k-bounded iff ∃k∈N∀M∈Mi:M(p)≤k. The PPN is said to be k-bounded iff every place of the PPN is k-bounded. We say thatPPN terminates properly if (∀M∈Mi∃Mx∈Mix:Mx∈M)∧Mi<ℵ0.A SNT process netPN=(P,T,A,AF,TP,RP,IP,OP,RMs) is said to besound iff the PPN=(P,T,A,AF,TP,RP,IP,OP,RMs,Mi) is k-bounded and it terminates properly for itsevery input markingMi.A SNT agent netAN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT) is said to besound iff the SNT process Petri net APN_=(P_,T_,A_,AF_,TP_,RP_,IP_,OP_,RM_s_,Mi) associated with the SNT agent Petri net APN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT,Mi) is sound.From many properties of the SNT process nets, respectively, SNT agent nets, we are especially interested in their soundness (in the terminology of the programming systems this property informally means that the programming system modeled by given process net will not cause deadlock [17] and memory or device overflow).We will start our study of the sound SNT process nets by introduction of so calledbase SNT process nets (BPN). BPN represent the class of PNs that are elementary sound (i.e., soundness of these PNs can be trivially proved).Figure5 shows six simple BPNs in their static markings Ms∈Ms (where x_n means nonempty finite sequence of the n nonnegative integer numbers; that is, x_n∈N0SQ, length(x_n)=n, n∈N, and in means nonempty finite sequence of the n nonnegative integer numbers i∈N0; that is, in∈N0SQ, in=i,i,…,i, and length(in)=n,n∈N. The BPNBASE1 is the simplest BPN at all and it contains only one place IOP that is simultaneously its input and output place (definition of PNs allows this case). BPNBASE3 can be used for the modeling of the programming statement IF… THEN… ELSE…. The BPNBASE4 then represents the model of the programming critical section, where typically Ms(R1)=1 in the resource place R1. The BPNBASE5 represents the synchronous method called mechanism where the called method is represented by the place P2. The BPNBASE6 can be used for the modelling of the programming barrier.Figure 5
Examples of base process nets.


### 2.2. Place-Substitution Operator and Its Properties

The place-substitution operator PLACE-SUBST is defined for the classes of PNs and ANs and it is shown to be conditionally preserving the soundness property. The sound PNs and ANs then form a closed set (i.e., the application of this operator on any two PNs or any couple of PN and AN with the soundness property resulting in another PN or AN with the soundness property). The design of a given programming system with the support of the place-substitution operator will such typically start with the BPNBASE1 and then it follows with the several place-substitution operations (i.e., substitution of the selected BPN over the place in the actual PN) with the support of selected BPNs that result into the complex SNT process net that models the part of the whole programming system.Definition 1.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) and PN2=(P2,T2,A2,AF2,TP2,RP2,IP2,  OP2,RMs2) be the PNs, and let p∈P1∖RP1 be a place of the PN PN1 such that (2)›p⊆›IP2∧OP2›⊆p›∨›p=p›=N∨›IP2=OP2›=N.The function PLACE-SUBST: PNET×PNET→PNET of the PN PN2 substitution over the place p of the PN PN1 will be denoted by PN1.pPN2. The execution of this function results in the new PN PN=(P,T,A,AF,TP,RP,IP,OP,RMs), where (i)
P=(P1∖{p})∪P2,(ii)
T=T1∪T2,(iii)
A=A2∪{(x,y)∈A1∣(x≠p)∨(y≠p)}∪{(x,IP2)∣(x,p)∈A1}∪{(OP2,y)∣(p,y)∈A1},(iv)
AF=AF2∪{((x,y),v)∈AF1∣(x≠p)∨(y≠p)}∪{((x,IP2),v)∣((x,p),v)∈AF1}∪{((OP2,y),v)∣((p,y),v)∈AF1},(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1, if p≠IP1; IP=IP2, if p=IP1,(viii)
OP=OP1, if p≠OP1; OP=OP2, if p=OP1,(ix)
RMs=RMs1⊗RMs2.Example 2.
The result of the place-substitution operationSN1.P2  SN2 where the place P2 of the BPN SN1 (see Figure 5) was substituted by the BPN SN2 can be shown in Figure 6. It is clear that all the necessary requests for the place-substitution operation are satisfied in this case, that is, P2 is not a resource place of the PN SN1, ›P2={4}⊆{4}=›IP2, IP2›={4}⊆{4}=P2›. It is easy to verify that in this case the resulting PN SN1.P2 SN2 is also sound.Figure 6
Result of place-substitution operationSN1.P2SN2.Lemma 3.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1), PN2=(P2,T2,A2,AF2,TP2,RP2,  IP2,OP2,RMs2), and PN3=(P3,T3,A3,AF3,TP3,RP3,IP3,OP3,RMs3) be the three PNs, let p1∈P1 be a place of the PN PN1 such that p1∉RP1, ((›p1⊆›IP2)∧(OP2›⊆p1›))∨(›p1=p1›=N)∨(›IP2=OP2›=N), and let p2∈P2 be a place of the PN PN2, such that p2∉RP2, ((›p2⊆›IP3)∧(OP3›⊆p2›))∨(›p2=p2›=N)∨(›IP3=OP3›=N). Then (3)PN1.p1PN2.p2PN3=PN1.p1PN2.p2PN3.Proof.
From Definition1 it directly follows that PN1.p1(PN2.p2PN3)   =  (PN1.p1PN2).p2PN3  =  (P,T,A,AF,TP,RP,IP,OP,RMs) where(i)
P=(P1∖{p1})∪(P2∖{p2})∪P3,(ii)
T=T1∪T2∪T3,(iii)
A=A3∪{(x,y)∈A2∣(x≠p2)∨(y≠p2)}∪{(x,IP3)∣(x,p2)∈A2}∪{(OP3,y)∣(p2,y)∈A2}  ∪  {(x,y)∈A1∣(x≠p1)∨(y≠p1)}∪{(x,IP2)∣(x,p1)∈A1}∪{(OP2,y)∣(p1,y)∈A1},(iv)
AF=AF3∪{((x,y),v)∈AF2∣(x≠p2)∨(y≠p2)}∪{((x,IP2),v)∣((x,p2),v)∈AF2}  ∪  {((OP2,y),v)∣((p,y2),v)∈AF2}∪{((x,y),v)∈AF1∣(x≠p)∨(y≠p)}∪{((x,IP2),v)∣((x,p),v)  ∈  AF1}∪{((OP2,y),v)∣((p,y),v)∈AF1},(v)
TP=TP1∪TP2∪TP3,(vi)
RP=RP1∪RP2∪RP3,(vii)
IP=IP1, if p1≠IP1; IP=IP2, if (p1=IP1)∧(p2≠IP2); IP=IP3, if (p1=IP1)∧(p2=IP2),(viii)
OP=OP1, if p1≠OP1; OP=OP2, if (p1=OP1)∧(p2≠OP2); IP=IP3, if (p1=OP1)∧(p2=OP2),(ix)
RMs=RMs1⊗RMs2⊗RMs3.Lemma 4.
The triple (PNET,PLACE-SUBST,BASE1) is a monoid.Proof.
Lemma4 is the direct consequence of Lemma 3 and it is clear that the BPNBASE1 (see Figure 5) is the neutral element of the monoid.Definition 5.
LetAN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1,OT1) be the AN and PN2=(P2,T2,A2,  AF2,TP2,RP2,IP2,OP2,RMs2) the PNs, and let p∈P1∖RP1 be a place of the AN AN1 such that (4)›p⊆›IP2∧OP2›⊆p›∨›p=p›=N∨›IP2=OP2›=N.The function PLACE-SUBST: ANET×PNET→ANET of the PN PN2 substitution over the place p of the AN AN1 will be denoted by AN1.pPN2. The execution of this function results in the new AN AN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT), where (i)
P=(P1∖{p})∪P2,(ii)
T=T1∪T2,(iii)
A=A2∪{(x,y)∈A1∣(x≠p)∨(y≠p)}∪{(x,IP2)∣(x,p)∈A1}∪{(OP2,y)∣(p,y)∈A1};(iv)
AF=AF2∪{((x,y),v)∈AF1∣(x≠p)∨(y≠p)}∪{((x,IP2),v)∣((x,p),v)∈AF1}  ∪  {((OP2,y),v)   ∣  ((p,y),v)∈AF1},(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1, if p≠IP1; IP=IP2, if p=IP1,(viii)
OP=OP1, if p≠OP1; OP=OP2, if p=OP1,(ix)
RMs=RMs1⊗RMs2,(x)
OT=OT1.Definition5 is similar to Definition 1 in the sense of overloading of the operator : PNET×PNET→PNET with the operator : ANET×PNET→ANET of the PN PN2 substitution over the place p of the AN AN1 which is denoted by AN1.pPN2. It is easy to formulate similar lemmas like Lemmas 3 and 4 for the case of this overloaded operator .We will investigate the necessary conditions for the soundness of the resulting SNT process or agent net in the following paragraphs. The first condition for the soundness of the resulting net is already in Definitions1 and 5; that is, the substituted place p∈P must not be a member of the set of the net resource places RP, p∉RP. Figure 7 shows the result of the resource place R1 (that contains the token 1 in the nonempty static marking Ms) of the sound net SN3 substitution by the sound net SN4, that is, the net SN3.R1SN4. The resulting net then does not satisfy the necessary conditions for its static marking Ms, because the token 1 is associated in this static marking Ms with the nonresource place IP2, and the transition T2 is then enabled in this static marking Ms which is not allowed. If we remove the token 1 from the place T2 then the resulting net is not sound again. So it is generally not possible to substitute any resource place of a given PN or AN by another PN.Figure 7
Result of place-substitution operationSN3.R1SN4.Figure8 shows the result of the place P2 of the sound net SN5 substitution by the sound net SN6, that is, the PN SN5.P2SN5, that is not sound. It can be seen for its input marking Mi, where Mi(IP1)=1′1. In this input marking Mi the transition T1 is enabled and its firing results into the marking M1, where MiT1M1. There is token 3 in the place P1 and the token 1 in the place P2 in the marking M1, and the transitions T2 and T5 are enabled in parallel in the marking M1 and after their parallel firing the PN results in the marking M2, where M1T2T5M2. In the marking M2 there will be the token 1 in the place OP2 and the token 3 in the place OP1. No transition is enabled in the nonoutput marking M2 and so the resulting net SN5.P2SN6 is not sound.Figure 8
Result of place-substitution operationSN5.P2SN6.The loss of the net soundness then follows from the existence of the arc(P1,T2) in the resulting net. The necessary condition for the soundness of the resulting net is in this case the following: ∀t∈P2•:((q∈•t)∧(q≠IP1))⇒(q•={t}) and it does not hold for the place P2 of the PNSN5, because transition T3∈P2• holds that ((P1∈•T3)∧(P1≠IP1)) and (P1•={T2,T3}). It is then clear that if the arc (P1,T2) is not present then the resulting net is sound.Figure9 shows the result of the place P2 of the sound net SN7 substitution by the sound net SN8, that is, the SNT process net SN7.P2SN8, that is again not sound. The loss of the soundness (it can be easily seen for any input marking Mi of the resulting PN) then follows from the fact that P2›={1,4}; that is, P2›>1. The necessary condition for the soundness of the resulting PN is in this case the following: P2›=1.Figure 9
Result of place-substitution operationSN7.P2SN8.Lemma 6.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) and PN2=(P2,T2,A2,AF2,TP2,RP2,IP2,  OP2,RMs2) be two sound PNs, and let p∈P1∖RP1 be a place of the PNPN1 such that ((›p⊆›IP2)∧(OP2›⊆p›))∨(›p=p›=N)∨(›IP2=OP2›=N), p›=1, ∀t∈p•:((q∈•t)∧(q≠IP1))  ⇒  (q•={t}). Then the PN PN1.pPN2 is also sound.Comment. If the conditions p∈P1∖RP1, ((›p⊆›IP2)∧(OP2›⊆p›))∨(›p=p›=N)∨(›IP2=OP2›=N), and p›=1, ∀t∈p•:((q∈•t)∧(q≠IP1))⇒(q•={t}) for the substituted place p∈P1 of the net PN1 are not satisfied the resulting net PN1.pPN2 does not need to be sound generally as follows from the previous three examples.Proof.
It is clear forp=IP1 or p=OP1 and it follows directly from the definition of the sound PN. Let p≠IP1 and p≠OP1. Because the PN PN1 is sound, it holds that ∀Mi∃k∈N∀q∈P1∀M∈Mi:M(q)≤k. This holds also for the substituted place p∈P1. From this follows that also the place IP2 in the resulting PN is k-bounded because the number of tokens in any reachable marking of the process PN1.pPN2 is at the highest equaling the number of tokens in the place p. Because the PN PN2 is also k-bounded and it terminates properly for any of its input markings Mi, from these facts follows that also the place OP2 in the resulting PN is k-bounded and so the whole PN PN1.pPN2 must be also k-bounded for any of its input markings Mi. Similarly, both PN PN1 and PN2 terminate properly for any of its input markings Mi. In particular for the PN PN1 holds true that ∀M∈Mi, M(p)≠∅, and ∃Mx:Mx∈M and for the PN PN2 holds true that ∀M∈Mi∃Mx:Mx∈M. The conditions p›=1, ∀t∈p•:((q∈•t)∧(q≠IP1))⇒(q•={t}) are satisfied for the PN PN1 and from these conditions follows that OP2›=1, ∀t∈OP2•:((q∈•t)∧(q≠IP1))⇒(q•={t}) in the resulting net PN1.pPN2. Then it follows that there must exist transition t, t∈OP2•, and the marking M of the resulting net PN1.pPN2 such that (M(OP2)≠∅)∧(tenM), because the PN PN1 terminates properly. So the whole PN PN1.pPN2 must also terminate properly for any of its input markings Mi and it is sound.It immediately follows from the previous lemma that the application of the operator PLACE-SUBST that satisfies all the necessary requests formulated in Lemma6 for two given sound PNs results into another sound PN.Lemma 7.
LetAN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1,OT1) be the sound AN and PN2=(P2,T2,A2,AF2,TP2,RP2,IP2,OP2,RMs2) the sound PN, and let p∈P1∖RP1 be a place of the AN AN1 such that ((›p⊆›IP2)∧(OP2›⊆p›))∨(›p=p›=N)∨(›IP2=OP2›=N), p›=1, ∀t∈p•:((q∈•t)  ∧  (q≠IP1))  ⇒  (q•={t}). Then the AN AN1.pPN2 is also sound.Proof.
Proof directly follows from the proof of Lemma6.


### 2.3. Asynchronous-Processing Operator and Its Properties

The asynchronous-processing operator ASYNC-PROC is the second operator defined for the class of all PNs and ANs and it is also shown to be preserving the soundness property. The sound PNs and ANs then form a closed set (i.e., the application of this operator on any couple of PN and AN or two ANs with the soundness property results in another PN or AN with the soundness property).Definition 8.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) be the PN and AN2=(P2,T2,A2,AF2,TP2,  RP2,IP2,OP2,RMs2,OT2) the AN, and let t1,t2,…,tn∈T1, n∈N, be the transitions of the PN PN1. The function ASYNC-PROC: PNET×ANET→PNET of the asynchronous-processing of the AN AN2 from the PN PN1 will be denoted by PN1.t1.t2.⋯.tn-AN2. The execution of this function results in the new PN PN=(P,T,A,AF,TP,RP,IP,OP,RMs), where (i)
P=P1∪P2,(ii)
T=T1∪T2,(iii)
A=A1∪A2∪{(t1,IP2)}∪{(t2,IP2)}∪⋯∪{(tn,IP2)},(iv)
AF=AF1∪AF2∪{((t1,IP2),k)}∪{((t2,IP2),m)}∪⋯∪{((tn,IP2),n)}, where k,m,n,…∈›IP2,(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1,(viii)
OP=OP1,(ix)
RMs=RMs1⊗RMs2.Example 9.
The result of the asynchronous-processing operationPN1.T1.T2-AN2 where both PN PN1 and AN AN2 are sound can be shown in Figure 10. It is clear that all the necessary requests for the asynchronous-processing operation are satisfied in this case. It is also easy to verify that in this case the resulting PNPN1.T1.T2-AN2 is also sound.Figure 10
Result of asynchronous-processing operationPN1.T1.T2-AN2.Lemma 10.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) is a PN, AN2=(P2,T2,A2,AF2,TP2,RP2,  IP2,OP2,RMs2,OT2) and AN3=(P3,T3,A3,AF3,TP3,RP3,IP3,OP3,RMs3,OT3) are two ANs, let t11,t21,…,tn1∈T1 are the transition of the PN PN1, n∈N, and t12,t22,…,tm2∈T2, m∈N, are the transition of the AN AN2. Then(5)PN1.t11⋯tn1-AN2.t12⋯tm2-AN3=PN1.t11⋯tn1-PN2.t12⋯tm2-PN3.Proof.
The proof is clear and follows directly from Definition8.Lemma 11.
The couple (PNET∪ANET, ASYNC-PROC) is a semigroup.Proof.
Lemma11 is the direct consequence of Lemma 10.Definition 12.
LetAN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1,OT1) and AN2=(P2,T2,A2,AF2,TP2,  RP2,IP2,OP2,RMs2,OT2) be the ANs, and let t1,t2,…,tn∈T1, n∈N, be the transitions of the AN AN1,AN1∩AN2=∅. The function ASYNC-PROC: ANET×ANET→ANET of the asynchronous-processing of the AN AN2 from the AN AN1 will be denoted by AN1.t1.t2.⋯.tn- AN2. The execution of this function results in the new AN AN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT), where(i)
P=P1∪P2,(ii)
T=T1∪T2,(iii)
A=A1∪A2∪{(t1,IP2)}∪{(t2,IP2)}∪⋯∪{(tn,IP2)},(iv)
AF=AF1∪AF2∪{((t1,IP2),k)}∪{((t2,IP2),m)}∪⋯∪{((tn,IP2),n)}, where k,m,n,…∈›IP2,(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1,(viii)
OP=OP1,(ix)
RMs=RMs1⊗RMs2(x)
OT=OT1.Definition12 is similar to Definition 8 in the sense of the overloading of the operator -: PNET×ANET→PNET with the operator -: ANET×ANET→ANET of the AN AN2 asynchronous-processing from the AN AN1. It is easy to formulate similar lemmas like Lemmas 10 and 11 for the case of this overloaded operator -.Lemma 13.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) be a sound PN and AN2=(P2,T2,A2,  AF2,TP2,RP2,IP2,OP2,RMs2,OT2) a sound AN, and let t1,t2,…,tn∈T1, n∈N, be the transitions of the PN PN1. Then the PN PN1.t1.t2.⋯.tn-AN2 is also sound.Proof.
Clear. Because the PNPN1 is sound, it holds that ∀Mi∃k∈N∀q∈P1∀M∈Mi:M(q)≤k. It also holds that ∀Mi∃t1t2⋯tm:Mit1M1t2M2⋯tmMx, m∈N, t1,t2,…,tm∈T1. From these facts follows that every of the transition t1,t2,…,tn∈T1, n∈N, will be fired finite times in every transition sequence Mit1M1t2M2⋯tmMx. From these immediately follows that in the resulting PN PN1.t1.t2.⋯.tn-AN2 is satisfied the condition ∀Mi∃k∈N∀M∈Mi:M(IP2)≤k. Because of the soundness of the AN AN2 the whole PN PN1.t1.t2.⋯.tn-AN2 must be bounded. Because the PN PN1 terminates properly for any of its input markings Mi and also the AN AN2 terminates properly and their firing of the transitions are independent it is clear that also the resulting PNPN1.t1.t2.⋯.tn-AN2 must terminate properly for any of its input marking and it is also sound.


### 2.4. Audiovisual Lecture Room with the Automatic Editing System

Within the MERLINGO project implementation the selected standard audiovisual lecture room was additionally outfitted with the automated editing system consisting of three good quality camerasSony BPE NEX-FS100EK series with theobject lens E18-200 mm to eliminate the problem of insufficient lighting in lecture rooms during recording (see Figure 11), followed by editing unitRoland VR-5 including three spatial microphonesRoland R-26 and control system with the motion sensors ofAMX 3100 line with the converterRS232/MiDi. That system ensures editing of video and audio signal read by the camera and microphone in the sectors where the lecturer is moving.Figure 11
Three cameras Sony BPE NEX-FS100EK.Additionally, this audiovisual lecture room has been outfitted with the programming systemEduArtenabling transfer of image (video) of the scanned person and transfer of presentation from the work station, interactive board, visualizer, and sound in the high resolution via the computer network of the sufficient bandwidth. The output is a recording viewable by the web browser. The integration of the whole unit is ensured by the control system of the AMX product line automated in such manner that the lecturer can concentrate on the context of their message and does not need to pay attention to control of presentation tools and means for the recording and transfer of the presentation into the resources of the central repository MERLINGO. There is no need for other persons to make a recording which is a cost saving feature and, additionally, the lecturer is not disturbed by them.For the realization of the automated editing were selected and implemented three basic types of shots:(i)
detail-view: lecturer (one or more) standing by the speaker’s desk; see Figure 12,(ii)
board-view: lecturer (one or more) are found in the zone of the board or in the zone between the speaker’s desk and board,(iii)
general-view: lecturer (one or more) are found outside the shotdetail-view orboard-view; see Figure 13.Figure 12
Shot ofdetail-view type in audiovisual lecture room.Figure 13
Shot ofgeneral-view type in audiovisual lecture room.


## 2.1. SNT Petri Process and Agent Nets and Their Properties

LetN denote the set of all natural numbers, N0 the set of all nonnegative integer numbers, ∅ the empty set, ⌐ the logical negation operator, A the cardinality of the given set A, where N=ℵ0, P(A) the family of all the subsets of a given set A, and IDENT the set of all identifiers over a certain alphabet.Multiset
M over a nonempty set S is a function m:S→N0. The nonnegative number m(a)∈N0, where a∈S, denotes the number of occurrences of the element a in the multiset m. The multiset m is usually represented by the formal sum ∑a∈Sma′a. SMS denotes the set of all nonempty multisets over the set S and SMSE denotes the set of all multisets over the set S.LetA be a nonempty set. By the (nonempty finite)sequenceσ over the set A a function σ can be understood, σ:{1,2,…,n}→A, where n∈N. The function ε:∅→A is called theempty sequence over the set A. The sequence σ:{1,2,…,n}→A is usually represented by the notation σ=a1,a2,…,an or σ=a1a2⋯an of the elements of the set A, where ai=σ(i) for 1≤i≤n. Empty sequence ε:∅→A over the set A is usually represented by the notation ε=. The set of all finite nonempty sequences over the set A is denoted by the notation ASQ and the set of allfinite (and possible empty) sequences over the set A by the notation ASQE. Thelength of the sequenceσ=a1,a2,…,an, where n∈N, is equal to the natural number n and the length of the empty sequence ε is equal to the number 0. The length of the sequence σ is represented by the notation length(σ). The function elem:ASQE→P(A), such that elem(σ)={a∣∃i:a=σ(i),  where1≤i≤length(σ)}, elem(ε)=∅, assigns to each sequence σ∈ASQE the set of all of itselements.LetA={a1,a2,…,an}, where n∈N, be a finite nonempty set.VectorV is a function V:A→N0. We will denote a vector V by the statement V=(V(1),V(2),…,V(n)).LetV={(V(1),V(2),…,V(n))∣V(i)∈N0for1≤i≤n} and W={(W(1),W(2),…,W(m))∣W(j)∈N0for1≤j≤m}. Then(1)
V
⊗
W
=
V
1
,
…
,
V
n
,
W
1
,
…
,
W
m
∣
V
i
∈
N
0
for
1
≤
i
≤
n
,
W
j
∈
N
0
for
1
≤
j
≤
m
,
i
f
V
≠
∅
∧
W
≠
∅
,
=
V
,
if
V
≠
∅
∧
W
=
∅
,
=
W
,
if
V
=
∅
∧
W
≠
∅
,
=
∅
,
i
f
V
=
∅
∧
W
=
∅
.It is clear that the operation ⊗ is associative (i.e., (V⊗W)⊗U=V⊗(W⊗U)).Asemigroup(S,⚪) is a set S together with an associative binary operation ⚪:S×S→S. Amonoid(M,⚪,u) is a semigroup (M,⚪) with an element u∈M such that ∀x∈M:u⚪x=x=x⚪u.Anet is an ordered triple NET=(P,T,A), where(i)
Pis a finite nonempty set ofplaces,(ii)
T is a finite set oftransitions, P∩T=∅,(iii)
A is a finite set ofarcs, A⊆(P×T)∪(T×P).A given net is then described with a bipartite graph containing a finite nonempty setP of places used for expressing conditions of a modeled system (we usually use circles for their representation), a finite set T of transitions describing changes in the modeled system (we usually draw them in the form of rectangles) and a finite set A of arcs being principally oriented while connecting a place with a transition or a transition with a place and we usually draw them as lines with arrows. We say then a net (P,T,A) isconnected iff it is not composed of two or more disjoint and nonempty nets.Some commonly used notations for the nets are•y={x∣(x,y)∈A} for thepreset and y•={x∣(y,x)∈A} for thepostset of a net element y (i.e., place or transition).ASNT net (single-number tokens net) is an ordered 5-tuple SNTN=(P,T,A,AF,TP), where(i)
(P,T,A) is a connected net, ∀p∈P:›p⊆›p,(ii)
AF is the arc function, AF:(P×T)∪(T×P)→N0SQE, AF(x,y)∈N0SQ iff (x,y)∈A, AFx,y= iff (x,y)∉A, where x,y∈P∪T,∀t∈T∃k∈N∀p∈(•t∪t•): length(AF(p,t))=length(AF(t,p))=k,(iii)
TP is the transition priority function, TP:T→N.The arc functionAF of a given SNT net assigns each arc with a (nonempty) sequence of the nonnegative integer numbers expressing a removed or added token from or to the place associated with that arc when executing a particular transition. There must be the only one length k(k∈N) of all the values of the arc function AF (i.e., for the sequences of nonnegative integer numbers) for the given transition t and all of its associated input and output arcs. Transition priority function TP of a given SNT net assigns with each transition the natural number value expressing its priority (transition priority function has the default value of 1 if it is not explicitly indicated in the SNT net diagram).LetSNTN=(P,T,A,AF,TP) be a SNT net and p∈P a place. We will define the sets ›p∈P(N) of theplace input tokens and p›∈P(N) of theplace output tokens by the following way:›p=def{elem(AF(t,p))∣t∈•p}, if •p≠∅,›p=defp›, if (•p=∅)∧(p•≠∅),›p=defN, if (•p=∅)∧(p•=∅),p›=def{elem(AF(p,t))∣t∈p•}, if p•≠∅,p›=def›p, if (p•=∅)∧(•p≠∅),p›=defN, if (•p=∅)∧(p•=∅).Then the condition›p⊆›p must be true for all the places p of the given SNT netSNTN.Marking
M of the SNT netSNTN is a mapping M:P→N0MSE such that ∀p∈P∀e∈M(p):e∈p› (i.e., every token e represents the chosen single nonnegative integer number and every token e that is associated with the place p in the marking M must be an element of the set p› of the place output tokens). Marking M of a given SNT net then assigns each place with the multiset over the set N0 of all the nonnegative integer numbers and we use the form of m for the single token representation in the net diagrams, where m∈N0. Marking M of the SNT net then expresses the current status of a process that is modeled by the given SNT net. If P={P1,P2,…,Pn}, where n∈N, then marking M of given SNT net can be written as a P-vector M=(M(P1),M(P2),…,M(Pn)).ASNT Petri net is an ordered couple SNTPN=(SNTN,M0), where SNTN=(P,T,A,AF,TP) is a SNT net and M0:P→N0MSE is an initial marking of the netSNTN. We will then also denote a SNT Petri net by an ordered 6-tuple SNTPN=(P,T,A,AF,TP,M0).Transitiont∈T isenabled in the marking M of the SNT Petri netSNTPN if ∃ind∈N∀p∈•t∃e∈M(p):e=AF(p,t)(ind) and we denote that fact symbolically in the form of t enM.Firing of the transitiont∈T results in changing the marking M into the marking M′, where ∀p∈P:M′p=Mp∖AFp,tind∪AFt,pind, that is, denoted by MtM′. Marking Mn+1 isreachable from the marking M1 iff there exists a finite sequence σ=t1t2⋯tn of the transitions, where t1,t2,…,tn∈T, n∈N, such that M1t1M2t2M3⋯MntnMn+1. The set of all the markings reachable from the marking M will be denoted by the symbol M. The set of all finite and infinite transition sequences that are reachable from the marking M will be denoted by the symbol [M⟫; that is, M=t1t2⋯tn∣∃Mn+1∈M:Mt1t2⋯tnMn+1,n∈N.Figure1 illustrates the SNT Petri net N1=(P,T,A,AF,TP,M0), where(i)
P={P1,P2,P3,P4},(ii)
T={T1},(iii)
A={(P1,T1),(P2,T1),(T1,P3),(T1,P4)},(iv)
AF={((P1,T1),2,1),((P2,T1),2,3),((T1,P3),1,2),((T1,P4),1,1)},(v)
TP={(T1,1)},(vi)
M0=3′1,1′3,1′2,∅.Figure 1
Firing of transition in SNT Petri netN1.It can be seen that∀t∈T∃k∈N∀p∈(•t∪t•): length(AF(p,t))=length(AF(t,p))=k for the net N1, because for the only one transition T1∈T∃2∈N∀p∈(•T1∪T1•): length(AF(p,t))=length(AF(t,p))=2; that is, for any given transition t∈T and for all its input arcs (p,t) and all its output arcs (t,p) must be all the values of the arc functions AF(p,t) and AF(t,p) the sequences with the equal length k.We can also determine thatP1›={1,2} (because P1•≠∅ and P1›=  {elem(AF(P1,T1))}={1,2}), ›P1={1,2} (because (•P1=∅)∧(P1•≠∅), ›P1=P1›), P2›={2,3}=›P2,  P3›={1,2}=›P3, and P4›=1=›P4. We can also verify that the condition ∀p∈P∀e∈M0(p):e∈p› is fully satisfied for the net N1.Transition T1 is enabled in the markingM0 of the SNT Petri net N1 because ∃ind∈N∀p  ∈  •T1∃e∈M(p):e=AF(p,T1)(ind), where ind=2, •T1={P1,P2}, AF(P1,T1)(2)=1∈2′1  +  1′4 =  M0(P1), and AF(P2,T1)(2)=3∈1′3=M0(P2). Firing of the transition T1 results in changing of the net marking M0 into the marking M1, M0T1M1, where M1=(1′1+1′4,∅,1′2+1′5,1′1), because we will remove the token 1 from the place P1 and the token 3 from the place P2 and then we will add the token 2 (i.e., AF(T1,P3)(2)) into the place P3 and the token 1 (i.e., AF(T1,P4)(2)) into the place P4 according to the firing of the transition general rule.When enabling individual transitions of a given SNT Petri net so calledconflicts can originate in its certain markings (or conflict transitions). At the enabling of transitions t1 and t2 of the given SNT Petri net in its marking M, where t1, t2∈T, the conflict occurs, if ((•t1∩•t2≠∅)∧(t1enM)  ∧  (t2enM)∧⌐({t1,t2}enM)). The term of the conflict transitions can be obviously easily generalized for the case of the finite set t1,t2,…,tn(n∈N) of transitions of a given SNT Petri net.A typical example of conflict transitions in the particular marking of the SNT Petri netN2 is shown in Figure 2. The transitions T1 and T2 have the common input place P1; both are enabled but not enabled in parallel. When solving such transitions conflicts we will therefore follow the rule which determines, informally said, from the set of conflict transitions the one which will be enabled, whose value of the transition priority function TP is the highest. If such transition from the set of conflict transitions does not exist, the given conflict would have to be solved by other means. Our studied example will be then on the basis of that rule the transition T2 enabled (because TP(T1)=1 and TP(T2)=2).Figure 2
Conflict transitions in SNT Petri netN2.ASNT process net (PN) is an ordered 9-tuple PN=(P,T,A,AF,TP,RP,IP,OP,RMs), where(i)
(P,T,A,AF,TP) is aconnected SNT net,(ii)
RP is a finite set ofresource places, RP⊂P,(iii)
theinput placeIP is the only one place IP∈(P∖RP) such that •IP=∅,(iv)
theoutput placeOP is the only one place OP∈(P∖RP) such that OP•=∅,(v)
RMs is the set of all the allowedresource static markings (see below).The finite set of the resource placesRP is used for expressing the conditions of a modeled system containing some initial resources and we use circles with the double line for their representation. The input place IP is the only one place from the set P∖RP of the nonresource places that has no input transition and similarly the output place OP is the only one place from the set P∖RP of the nonresource places of the SNT process net that has no output transition. The class of all the SNT process nets will be denoted by the symbol PNET.Marking
M of the SNT process net PN is again a mapping M:P→N0MSE such that ∀p∈P∀e∈M(p):e∈p›. If RP={R1,R2,…,Rm}, where m∈N, P∖RP={IP,P1,P2,…,Pn,OP}, where n∈N, then the marking M can be written as a P-vector M=(M(IP),M(P1),M(P2),…,M(Pn),M(R1),  M(R2),…,M(Rm),M(OP)).Static marking
M
s of the SNT process net PN is a marking Ms such that ∀p∉RP:Ms(p)=∅; ∀t∈T:⌐(tenMs); that is, informally said, in the static marking Ms the tokens are allowed in the chosen resource places only and no transition is enabled in this static marking Ms. Static marking Ms of the SNT process net PN can then be written as a P-vector Ms=(∅,∅,∅,…,∅,Ms(R1),Ms(R2),…,Ms(Rm),∅). The set of all the allowed static markings Ms of the SNT process net PN we will denote by the symbol Ms.IfMs is the given static marking of the SNT process net PN, then by the symbol RMs we denote theresource static marking associated with the static marking Ms, that is, the function RMs:RP→N0MSE, where ∀p∈RP:RMs(p)=Ms(p) (i.e., informally said, resource static marking RMs associated with the static marking Ms of the SNT process net PN is the vector containing only the resource places markings of the static marking Ms and the static marking Ms of all the remaining places of the net PN is then equal to the empty set ∅). If RP={R1,R2,…,Rm}, where m∈N, then the resource static marking RMs of the SNT process net PN can be written as a RP vector RMs=(RMs(R1),RMs(R2),…,RMs(Rm)). The set of all the allowed resource static markings RMs associated with the set Ms of all allowed static markings Ms of the SNT process net PN will be denoted by the symbol RMs.Input marking
M
i of the SNT process net PN is a marking Mi such that Mi(IP)≠∅, Mi(OP)=∅, ∃Ms∈Ms∀p∈(P∖{IP,OP}):Mi(p)=Ms(p); that is, informally said, in the input marking Mi the input place IP must contain at least one token, the output place OP must not contain any token, and the marking Mi of the remaining places corresponds with the chosen static marking Ms from the set of all the allowed static markings Ms. We will denote this chosen static marking Ms∈Ms associated with the given input marking Mi by the symbol Msi. Input marking Mi of the process net PN can then be written as a P-vector Mi=(Mi(IP),∅,∅,…,∅,Msi(R1),Msi(R2),…,Msi(Rm),∅).Output (exit) marking
M
x reachable from the input marking Mi of the SNT process net PN is a marking Mx such that Mx(IP)=∅, Mx∈Mi, Mx(OP)=Mi(IP), and ∃Ms′∈Ms∀p∈(P∖{IP,OP}):Mx(p)  =  Ms′(p); that is, informally said, in the output marking Mx the input place IP must not contain any token, the output marking Mx is reachable from the input marking Mi, the output place OP must contain the same number of tokens in the output marking Mx as the input place IP in the input marking Mi and the markings of the remaining places correspond with the chosen static marking Ms′ from the set of allowed static markings Ms. We will denote this chosen static marking Ms′∈Ms associated with the given output marking Mx by the symbol Ms′x. Output marking Mx of the SNT process net PN can then be written as a P-vector Mx=(∅,∅,∅,…,∅,Ms′x(R1),Ms′x(R2),…,Ms′x(Rm),Mx(OP)). The set of all the output markings Mx that are reachable from the input marking Mi of the SNT process net PN will be denoted by the symbol Mix.Figure3 illustrates the SNT process net N3, where RP={R1} is the only one resource place of the net, IP is the input place IP, OP is the output place OP, and the set RMs of all its allowed resource static markings RMs={(1′1)}, in its static Ms, input Mi, and output Mx markings (note the resource place R1 with the initial token in the static marking Ms) where no transition must be enabled in (any) static marking Ms.Figure 3
Static, input, and output markings of the SNT process netN3.ASNT process Petri net is an ordered couple PPN=(PN,Mi), where PN=(P,T,A,AF,TP,RP,IP,OP,RMs) is a SNT process net and Mi is an input marking of the PN. We will then also denote a SNT process Petri net by an ordered 10-tuple PPN=(P,T,A,AF,TP,RP,IP,OP,RMs,Mi).ASNT agent net (AN) is an ordered 10-tuple AN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT), where(i)
(P,T,A,AF,TP) is aconnected SNT net,(ii)
RP is a finite set ofresource places, RP⊂P,(iii)
theinput placeIP is the only one place IP∈(P∖RP) such that •IP=∅,(iv)
theoutput placeOP is the selected place OP∈(P∖RP) such that OP•={OT},(v)
RMs is the set of all the allowedresource static markings,(vi)
theoutput transitionOT is the selected transition OT∈T such that •OT={OP}, TP(OT)=1.The concept of the SNT agent net such extends the concept of the SNT process net. So, informally said, the output placeOP is the selected place of the SNT agent net that has the single output transition OT and the output transition OT is the selected transition of the SNT agent net that has the single input place OP; it has no one output place and its transition priority function TP value is always the natural number 1. The meanings of the marking M, the static marking Ms, the input marking Mi, and the output marking Mx of the SNT agent net AN are the same as in the case of the SNT process net PN. The class of all the SNT agent nets will be denoted by the symbol ANET.Figure4 illustrates the SNT agent net N3, where RP={R1} is the only one resource place, IP is the input place IP, OP is the output place OP, OT is the output transition OT, and the set RMs of all its allowed resource static markings RMs={(1′1)}, in its input marking Mi.Figure 4
SNT agent netN4.LetAN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT) be a SNT agent net. The SNT process net AN_ associated with the SNT agent netAN is the 9-tuple AN_=(P_,T_,A_,AF_,TP_,RP_,IP_,OP_,RM_s_), where P_=P, T_=T∖{OT}, A_=A∖{(OP,OT)}, AF_=AF∖{((OP,OT),k)∣k∈N}, TP_=TP∖{(OT,1)}, RP_=RP, IP_=IP, OP_=OP, and RM_s_=RMs.ASNT agent Petri net is an ordered couple APN=(AN,Mi), where AN=(P,T,A,AF,TP,RP,IP,OP,   RMs,OT) is a SNT agent net and Mi is an input marking of the AN. We will then also denote a SNT agent Petri net by an ordered 11-tuple APN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT,Mi). A SNT process Petri net APN_=(AN_,Mi) is associated with the SNT agent Petri net APN=(AN,Mi).LetPPN=(P,T,A,AF,TP,RP,IP,OP,RMs,Mi) be a SNT process Petri net. A place p∈P is said to be k-bounded iff ∃k∈N∀M∈Mi:M(p)≤k. The PPN is said to be k-bounded iff every place of the PPN is k-bounded. We say thatPPN terminates properly if (∀M∈Mi∃Mx∈Mix:Mx∈M)∧Mi<ℵ0.A SNT process netPN=(P,T,A,AF,TP,RP,IP,OP,RMs) is said to besound iff the PPN=(P,T,A,AF,TP,RP,IP,OP,RMs,Mi) is k-bounded and it terminates properly for itsevery input markingMi.A SNT agent netAN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT) is said to besound iff the SNT process Petri net APN_=(P_,T_,A_,AF_,TP_,RP_,IP_,OP_,RM_s_,Mi) associated with the SNT agent Petri net APN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT,Mi) is sound.From many properties of the SNT process nets, respectively, SNT agent nets, we are especially interested in their soundness (in the terminology of the programming systems this property informally means that the programming system modeled by given process net will not cause deadlock [17] and memory or device overflow).We will start our study of the sound SNT process nets by introduction of so calledbase SNT process nets (BPN). BPN represent the class of PNs that are elementary sound (i.e., soundness of these PNs can be trivially proved).Figure5 shows six simple BPNs in their static markings Ms∈Ms (where x_n means nonempty finite sequence of the n nonnegative integer numbers; that is, x_n∈N0SQ, length(x_n)=n, n∈N, and in means nonempty finite sequence of the n nonnegative integer numbers i∈N0; that is, in∈N0SQ, in=i,i,…,i, and length(in)=n,n∈N. The BPNBASE1 is the simplest BPN at all and it contains only one place IOP that is simultaneously its input and output place (definition of PNs allows this case). BPNBASE3 can be used for the modeling of the programming statement IF… THEN… ELSE…. The BPNBASE4 then represents the model of the programming critical section, where typically Ms(R1)=1 in the resource place R1. The BPNBASE5 represents the synchronous method called mechanism where the called method is represented by the place P2. The BPNBASE6 can be used for the modelling of the programming barrier.Figure 5
Examples of base process nets.


## 2.2. Place-Substitution Operator and Its Properties

The place-substitution operator PLACE-SUBST is defined for the classes of PNs and ANs and it is shown to be conditionally preserving the soundness property. The sound PNs and ANs then form a closed set (i.e., the application of this operator on any two PNs or any couple of PN and AN with the soundness property resulting in another PN or AN with the soundness property). The design of a given programming system with the support of the place-substitution operator will such typically start with the BPNBASE1 and then it follows with the several place-substitution operations (i.e., substitution of the selected BPN over the place in the actual PN) with the support of selected BPNs that result into the complex SNT process net that models the part of the whole programming system.Definition 1.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) and PN2=(P2,T2,A2,AF2,TP2,RP2,IP2,  OP2,RMs2) be the PNs, and let p∈P1∖RP1 be a place of the PN PN1 such that (2)›p⊆›IP2∧OP2›⊆p›∨›p=p›=N∨›IP2=OP2›=N.The function PLACE-SUBST: PNET×PNET→PNET of the PN PN2 substitution over the place p of the PN PN1 will be denoted by PN1.pPN2. The execution of this function results in the new PN PN=(P,T,A,AF,TP,RP,IP,OP,RMs), where (i)
P=(P1∖{p})∪P2,(ii)
T=T1∪T2,(iii)
A=A2∪{(x,y)∈A1∣(x≠p)∨(y≠p)}∪{(x,IP2)∣(x,p)∈A1}∪{(OP2,y)∣(p,y)∈A1},(iv)
AF=AF2∪{((x,y),v)∈AF1∣(x≠p)∨(y≠p)}∪{((x,IP2),v)∣((x,p),v)∈AF1}∪{((OP2,y),v)∣((p,y),v)∈AF1},(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1, if p≠IP1; IP=IP2, if p=IP1,(viii)
OP=OP1, if p≠OP1; OP=OP2, if p=OP1,(ix)
RMs=RMs1⊗RMs2.Example 2.
The result of the place-substitution operationSN1.P2  SN2 where the place P2 of the BPN SN1 (see Figure 5) was substituted by the BPN SN2 can be shown in Figure 6. It is clear that all the necessary requests for the place-substitution operation are satisfied in this case, that is, P2 is not a resource place of the PN SN1, ›P2={4}⊆{4}=›IP2, IP2›={4}⊆{4}=P2›. It is easy to verify that in this case the resulting PN SN1.P2 SN2 is also sound.Figure 6
Result of place-substitution operationSN1.P2SN2.Lemma 3.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1), PN2=(P2,T2,A2,AF2,TP2,RP2,  IP2,OP2,RMs2), and PN3=(P3,T3,A3,AF3,TP3,RP3,IP3,OP3,RMs3) be the three PNs, let p1∈P1 be a place of the PN PN1 such that p1∉RP1, ((›p1⊆›IP2)∧(OP2›⊆p1›))∨(›p1=p1›=N)∨(›IP2=OP2›=N), and let p2∈P2 be a place of the PN PN2, such that p2∉RP2, ((›p2⊆›IP3)∧(OP3›⊆p2›))∨(›p2=p2›=N)∨(›IP3=OP3›=N). Then (3)PN1.p1PN2.p2PN3=PN1.p1PN2.p2PN3.Proof.
From Definition1 it directly follows that PN1.p1(PN2.p2PN3)   =  (PN1.p1PN2).p2PN3  =  (P,T,A,AF,TP,RP,IP,OP,RMs) where(i)
P=(P1∖{p1})∪(P2∖{p2})∪P3,(ii)
T=T1∪T2∪T3,(iii)
A=A3∪{(x,y)∈A2∣(x≠p2)∨(y≠p2)}∪{(x,IP3)∣(x,p2)∈A2}∪{(OP3,y)∣(p2,y)∈A2}  ∪  {(x,y)∈A1∣(x≠p1)∨(y≠p1)}∪{(x,IP2)∣(x,p1)∈A1}∪{(OP2,y)∣(p1,y)∈A1},(iv)
AF=AF3∪{((x,y),v)∈AF2∣(x≠p2)∨(y≠p2)}∪{((x,IP2),v)∣((x,p2),v)∈AF2}  ∪  {((OP2,y),v)∣((p,y2),v)∈AF2}∪{((x,y),v)∈AF1∣(x≠p)∨(y≠p)}∪{((x,IP2),v)∣((x,p),v)  ∈  AF1}∪{((OP2,y),v)∣((p,y),v)∈AF1},(v)
TP=TP1∪TP2∪TP3,(vi)
RP=RP1∪RP2∪RP3,(vii)
IP=IP1, if p1≠IP1; IP=IP2, if (p1=IP1)∧(p2≠IP2); IP=IP3, if (p1=IP1)∧(p2=IP2),(viii)
OP=OP1, if p1≠OP1; OP=OP2, if (p1=OP1)∧(p2≠OP2); IP=IP3, if (p1=OP1)∧(p2=OP2),(ix)
RMs=RMs1⊗RMs2⊗RMs3.Lemma 4.
The triple (PNET,PLACE-SUBST,BASE1) is a monoid.Proof.
Lemma4 is the direct consequence of Lemma 3 and it is clear that the BPNBASE1 (see Figure 5) is the neutral element of the monoid.Definition 5.
LetAN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1,OT1) be the AN and PN2=(P2,T2,A2,  AF2,TP2,RP2,IP2,OP2,RMs2) the PNs, and let p∈P1∖RP1 be a place of the AN AN1 such that (4)›p⊆›IP2∧OP2›⊆p›∨›p=p›=N∨›IP2=OP2›=N.The function PLACE-SUBST: ANET×PNET→ANET of the PN PN2 substitution over the place p of the AN AN1 will be denoted by AN1.pPN2. The execution of this function results in the new AN AN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT), where (i)
P=(P1∖{p})∪P2,(ii)
T=T1∪T2,(iii)
A=A2∪{(x,y)∈A1∣(x≠p)∨(y≠p)}∪{(x,IP2)∣(x,p)∈A1}∪{(OP2,y)∣(p,y)∈A1};(iv)
AF=AF2∪{((x,y),v)∈AF1∣(x≠p)∨(y≠p)}∪{((x,IP2),v)∣((x,p),v)∈AF1}  ∪  {((OP2,y),v)   ∣  ((p,y),v)∈AF1},(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1, if p≠IP1; IP=IP2, if p=IP1,(viii)
OP=OP1, if p≠OP1; OP=OP2, if p=OP1,(ix)
RMs=RMs1⊗RMs2,(x)
OT=OT1.Definition5 is similar to Definition 1 in the sense of overloading of the operator : PNET×PNET→PNET with the operator : ANET×PNET→ANET of the PN PN2 substitution over the place p of the AN AN1 which is denoted by AN1.pPN2. It is easy to formulate similar lemmas like Lemmas 3 and 4 for the case of this overloaded operator .We will investigate the necessary conditions for the soundness of the resulting SNT process or agent net in the following paragraphs. The first condition for the soundness of the resulting net is already in Definitions1 and 5; that is, the substituted place p∈P must not be a member of the set of the net resource places RP, p∉RP. Figure 7 shows the result of the resource place R1 (that contains the token 1 in the nonempty static marking Ms) of the sound net SN3 substitution by the sound net SN4, that is, the net SN3.R1SN4. The resulting net then does not satisfy the necessary conditions for its static marking Ms, because the token 1 is associated in this static marking Ms with the nonresource place IP2, and the transition T2 is then enabled in this static marking Ms which is not allowed. If we remove the token 1 from the place T2 then the resulting net is not sound again. So it is generally not possible to substitute any resource place of a given PN or AN by another PN.Figure 7
Result of place-substitution operationSN3.R1SN4.Figure8 shows the result of the place P2 of the sound net SN5 substitution by the sound net SN6, that is, the PN SN5.P2SN5, that is not sound. It can be seen for its input marking Mi, where Mi(IP1)=1′1. In this input marking Mi the transition T1 is enabled and its firing results into the marking M1, where MiT1M1. There is token 3 in the place P1 and the token 1 in the place P2 in the marking M1, and the transitions T2 and T5 are enabled in parallel in the marking M1 and after their parallel firing the PN results in the marking M2, where M1T2T5M2. In the marking M2 there will be the token 1 in the place OP2 and the token 3 in the place OP1. No transition is enabled in the nonoutput marking M2 and so the resulting net SN5.P2SN6 is not sound.Figure 8
Result of place-substitution operationSN5.P2SN6.The loss of the net soundness then follows from the existence of the arc(P1,T2) in the resulting net. The necessary condition for the soundness of the resulting net is in this case the following: ∀t∈P2•:((q∈•t)∧(q≠IP1))⇒(q•={t}) and it does not hold for the place P2 of the PNSN5, because transition T3∈P2• holds that ((P1∈•T3)∧(P1≠IP1)) and (P1•={T2,T3}). It is then clear that if the arc (P1,T2) is not present then the resulting net is sound.Figure9 shows the result of the place P2 of the sound net SN7 substitution by the sound net SN8, that is, the SNT process net SN7.P2SN8, that is again not sound. The loss of the soundness (it can be easily seen for any input marking Mi of the resulting PN) then follows from the fact that P2›={1,4}; that is, P2›>1. The necessary condition for the soundness of the resulting PN is in this case the following: P2›=1.Figure 9
Result of place-substitution operationSN7.P2SN8.Lemma 6.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) and PN2=(P2,T2,A2,AF2,TP2,RP2,IP2,  OP2,RMs2) be two sound PNs, and let p∈P1∖RP1 be a place of the PNPN1 such that ((›p⊆›IP2)∧(OP2›⊆p›))∨(›p=p›=N)∨(›IP2=OP2›=N), p›=1, ∀t∈p•:((q∈•t)∧(q≠IP1))  ⇒  (q•={t}). Then the PN PN1.pPN2 is also sound.Comment. If the conditions p∈P1∖RP1, ((›p⊆›IP2)∧(OP2›⊆p›))∨(›p=p›=N)∨(›IP2=OP2›=N), and p›=1, ∀t∈p•:((q∈•t)∧(q≠IP1))⇒(q•={t}) for the substituted place p∈P1 of the net PN1 are not satisfied the resulting net PN1.pPN2 does not need to be sound generally as follows from the previous three examples.Proof.
It is clear forp=IP1 or p=OP1 and it follows directly from the definition of the sound PN. Let p≠IP1 and p≠OP1. Because the PN PN1 is sound, it holds that ∀Mi∃k∈N∀q∈P1∀M∈Mi:M(q)≤k. This holds also for the substituted place p∈P1. From this follows that also the place IP2 in the resulting PN is k-bounded because the number of tokens in any reachable marking of the process PN1.pPN2 is at the highest equaling the number of tokens in the place p. Because the PN PN2 is also k-bounded and it terminates properly for any of its input markings Mi, from these facts follows that also the place OP2 in the resulting PN is k-bounded and so the whole PN PN1.pPN2 must be also k-bounded for any of its input markings Mi. Similarly, both PN PN1 and PN2 terminate properly for any of its input markings Mi. In particular for the PN PN1 holds true that ∀M∈Mi, M(p)≠∅, and ∃Mx:Mx∈M and for the PN PN2 holds true that ∀M∈Mi∃Mx:Mx∈M. The conditions p›=1, ∀t∈p•:((q∈•t)∧(q≠IP1))⇒(q•={t}) are satisfied for the PN PN1 and from these conditions follows that OP2›=1, ∀t∈OP2•:((q∈•t)∧(q≠IP1))⇒(q•={t}) in the resulting net PN1.pPN2. Then it follows that there must exist transition t, t∈OP2•, and the marking M of the resulting net PN1.pPN2 such that (M(OP2)≠∅)∧(tenM), because the PN PN1 terminates properly. So the whole PN PN1.pPN2 must also terminate properly for any of its input markings Mi and it is sound.It immediately follows from the previous lemma that the application of the operator PLACE-SUBST that satisfies all the necessary requests formulated in Lemma6 for two given sound PNs results into another sound PN.Lemma 7.
LetAN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1,OT1) be the sound AN and PN2=(P2,T2,A2,AF2,TP2,RP2,IP2,OP2,RMs2) the sound PN, and let p∈P1∖RP1 be a place of the AN AN1 such that ((›p⊆›IP2)∧(OP2›⊆p›))∨(›p=p›=N)∨(›IP2=OP2›=N), p›=1, ∀t∈p•:((q∈•t)  ∧  (q≠IP1))  ⇒  (q•={t}). Then the AN AN1.pPN2 is also sound.Proof.
Proof directly follows from the proof of Lemma6.


## 2.3. Asynchronous-Processing Operator and Its Properties

The asynchronous-processing operator ASYNC-PROC is the second operator defined for the class of all PNs and ANs and it is also shown to be preserving the soundness property. The sound PNs and ANs then form a closed set (i.e., the application of this operator on any couple of PN and AN or two ANs with the soundness property results in another PN or AN with the soundness property).Definition 8.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) be the PN and AN2=(P2,T2,A2,AF2,TP2,  RP2,IP2,OP2,RMs2,OT2) the AN, and let t1,t2,…,tn∈T1, n∈N, be the transitions of the PN PN1. The function ASYNC-PROC: PNET×ANET→PNET of the asynchronous-processing of the AN AN2 from the PN PN1 will be denoted by PN1.t1.t2.⋯.tn-AN2. The execution of this function results in the new PN PN=(P,T,A,AF,TP,RP,IP,OP,RMs), where (i)
P=P1∪P2,(ii)
T=T1∪T2,(iii)
A=A1∪A2∪{(t1,IP2)}∪{(t2,IP2)}∪⋯∪{(tn,IP2)},(iv)
AF=AF1∪AF2∪{((t1,IP2),k)}∪{((t2,IP2),m)}∪⋯∪{((tn,IP2),n)}, where k,m,n,…∈›IP2,(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1,(viii)
OP=OP1,(ix)
RMs=RMs1⊗RMs2.Example 9.
The result of the asynchronous-processing operationPN1.T1.T2-AN2 where both PN PN1 and AN AN2 are sound can be shown in Figure 10. It is clear that all the necessary requests for the asynchronous-processing operation are satisfied in this case. It is also easy to verify that in this case the resulting PNPN1.T1.T2-AN2 is also sound.Figure 10
Result of asynchronous-processing operationPN1.T1.T2-AN2.Lemma 10.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) is a PN, AN2=(P2,T2,A2,AF2,TP2,RP2,  IP2,OP2,RMs2,OT2) and AN3=(P3,T3,A3,AF3,TP3,RP3,IP3,OP3,RMs3,OT3) are two ANs, let t11,t21,…,tn1∈T1 are the transition of the PN PN1, n∈N, and t12,t22,…,tm2∈T2, m∈N, are the transition of the AN AN2. Then(5)PN1.t11⋯tn1-AN2.t12⋯tm2-AN3=PN1.t11⋯tn1-PN2.t12⋯tm2-PN3.Proof.
The proof is clear and follows directly from Definition8.Lemma 11.
The couple (PNET∪ANET, ASYNC-PROC) is a semigroup.Proof.
Lemma11 is the direct consequence of Lemma 10.Definition 12.
LetAN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1,OT1) and AN2=(P2,T2,A2,AF2,TP2,  RP2,IP2,OP2,RMs2,OT2) be the ANs, and let t1,t2,…,tn∈T1, n∈N, be the transitions of the AN AN1,AN1∩AN2=∅. The function ASYNC-PROC: ANET×ANET→ANET of the asynchronous-processing of the AN AN2 from the AN AN1 will be denoted by AN1.t1.t2.⋯.tn- AN2. The execution of this function results in the new AN AN=(P,T,A,AF,TP,RP,IP,OP,RMs,OT), where(i)
P=P1∪P2,(ii)
T=T1∪T2,(iii)
A=A1∪A2∪{(t1,IP2)}∪{(t2,IP2)}∪⋯∪{(tn,IP2)},(iv)
AF=AF1∪AF2∪{((t1,IP2),k)}∪{((t2,IP2),m)}∪⋯∪{((tn,IP2),n)}, where k,m,n,…∈›IP2,(v)
TP=TP1∪TP2,(vi)
RP=RP1∪RP2,(vii)
IP=IP1,(viii)
OP=OP1,(ix)
RMs=RMs1⊗RMs2(x)
OT=OT1.Definition12 is similar to Definition 8 in the sense of the overloading of the operator -: PNET×ANET→PNET with the operator -: ANET×ANET→ANET of the AN AN2 asynchronous-processing from the AN AN1. It is easy to formulate similar lemmas like Lemmas 10 and 11 for the case of this overloaded operator -.Lemma 13.
LetPN1=(P1,T1,A1,AF1,TP1,RP1,IP1,OP1,RMs1) be a sound PN and AN2=(P2,T2,A2,  AF2,TP2,RP2,IP2,OP2,RMs2,OT2) a sound AN, and let t1,t2,…,tn∈T1, n∈N, be the transitions of the PN PN1. Then the PN PN1.t1.t2.⋯.tn-AN2 is also sound.Proof.
Clear. Because the PNPN1 is sound, it holds that ∀Mi∃k∈N∀q∈P1∀M∈Mi:M(q)≤k. It also holds that ∀Mi∃t1t2⋯tm:Mit1M1t2M2⋯tmMx, m∈N, t1,t2,…,tm∈T1. From these facts follows that every of the transition t1,t2,…,tn∈T1, n∈N, will be fired finite times in every transition sequence Mit1M1t2M2⋯tmMx. From these immediately follows that in the resulting PN PN1.t1.t2.⋯.tn-AN2 is satisfied the condition ∀Mi∃k∈N∀M∈Mi:M(IP2)≤k. Because of the soundness of the AN AN2 the whole PN PN1.t1.t2.⋯.tn-AN2 must be bounded. Because the PN PN1 terminates properly for any of its input markings Mi and also the AN AN2 terminates properly and their firing of the transitions are independent it is clear that also the resulting PNPN1.t1.t2.⋯.tn-AN2 must terminate properly for any of its input marking and it is also sound.


## 2.4. Audiovisual Lecture Room with the Automatic Editing System

Within the MERLINGO project implementation the selected standard audiovisual lecture room was additionally outfitted with the automated editing system consisting of three good quality camerasSony BPE NEX-FS100EK series with theobject lens E18-200 mm to eliminate the problem of insufficient lighting in lecture rooms during recording (see Figure 11), followed by editing unitRoland VR-5 including three spatial microphonesRoland R-26 and control system with the motion sensors ofAMX 3100 line with the converterRS232/MiDi. That system ensures editing of video and audio signal read by the camera and microphone in the sectors where the lecturer is moving.Figure 11
Three cameras Sony BPE NEX-FS100EK.Additionally, this audiovisual lecture room has been outfitted with the programming systemEduArtenabling transfer of image (video) of the scanned person and transfer of presentation from the work station, interactive board, visualizer, and sound in the high resolution via the computer network of the sufficient bandwidth. The output is a recording viewable by the web browser. The integration of the whole unit is ensured by the control system of the AMX product line automated in such manner that the lecturer can concentrate on the context of their message and does not need to pay attention to control of presentation tools and means for the recording and transfer of the presentation into the resources of the central repository MERLINGO. There is no need for other persons to make a recording which is a cost saving feature and, additionally, the lecturer is not disturbed by them.For the realization of the automated editing were selected and implemented three basic types of shots:(i)
detail-view: lecturer (one or more) standing by the speaker’s desk; see Figure 12,(ii)
board-view: lecturer (one or more) are found in the zone of the board or in the zone between the speaker’s desk and board,(iii)
general-view: lecturer (one or more) are found outside the shotdetail-view orboard-view; see Figure 13.Figure 12
Shot ofdetail-view type in audiovisual lecture room.Figure 13
Shot ofgeneral-view type in audiovisual lecture room.


## 3. Results and Discussion

The SNT process and agent net formal theory have been used at the design, verification, simulation, and implementation phases of software support of the audiovisual lecture room enabling automated recordings of the presentations including automated editing.When the speaker enters or exits one of thegeneral-view,board-view, ordetail-view areas the corresponding area sensor in the audiovisual lecture room sends the message describing this event. We will model these events by the tokens 1–6 in the resulting PNRNET by the following way:1
entry of the speaker into thegeneral-view area (from the nonscanned area of the lecture room),2
exit of the speaker outside thegeneral-view area (into the nonscanned area of the lecture room),3
exit of the speaker outside thegeneral-view area and entry of this speaker into theboard-view area,4
exit of the speaker outside theboard-view area and entry of this speaker into thegeneral-view area,5
exit of the speaker outside theboard-view area and entry of this speaker into thedetail-view area,6
exit of the speaker outside thedetail-view area and entry of this speaker into theboard-view area.The PNROOM1 in Figure 14(a) then models the basic functionalities of the lecture room during the presenter(s) entry or exit into or outside thegeneral-view area from or into the nonscanned area of the lecture room. The individual speaker that enters into thegeneral-view area is represented by the token 10 in the input place IP1 of the PNROOM1 in its input marking Mi. The input place IP1 can contain in its input marking Mi any finite number of these tokens. The firing of the transition T1 then represents an entry of the selected speaker into thegeneral-view area from the nonscanned area of the lecture room. This entry then generates the activity of the chosengeneral-view area sensor that is modeled by the message represented by the token 1 in the resulting PN. Speaker can then leave out thegeneral-view area into the nonscanned area of the lecture room by the firing of the transition T3 (the message represented by the token 2 will be sent by the selectedgeneral-view area sensor as the consequence of this action). The transition T2 is executed when the speaker leaves out thegeneral-view and then he enters into the remaining areas of the lecture room. The token 10 that represents the chosen speaker inside the lecture room will be changed into the token 20 after the firing of the transition T2. This change of the token after the firing of the transition T2 will such disable the possibility of the infinite transitions sequence T2T2⋯ that can be potentially fired by every token 10 in the marking of the place P2. Every token 20 in the actual marking of the place P2 can then enable only the transition T3 that models leaving out thegeneral-view area into the nonscanned area of the lecture room by the given speaker. It is clear that the PNROOM1 is sound for every one of its input markings Mi.Figure 14
SNT process netsROOM1 andROOM2.
(a)
(b)The PNROOM2 in Figure 14(b) then models the basic functionalities of the lecture room during the presenter(s) entry or exit into or outsideboard-view (represented by the place P10 and output place OP2) anddetail-view (represented by the place P11) areas. The token(s) 10 in the marking of the input place IP2 represent(s) individual speaker(s) in thegeneral-view area of the lecture room. The firing of the transition T10 models the entry into theboard-view area by the individual speaker and sending of the message represented by the token 3. The entry into thedetail-view area by the individual speaker and sending of the message represented by the token 5 is then modeled by the firing of the transition T12. Every presenter has the possibility of revisiting theboard-view area during its presentation (firing of the transition T11 and sending of the message 6) and returning again into thedetail-view area (firing of the transition T13 and sending of the message 5). Every such speaker is then represented by the token 30 after the firing of the transition T11 to prevent the possibility of the infinite transitions sequence T11T13T11T13⋯. The firing of the transition T14 and sending of the message represented by the token 4 then model an entry of the selected speaker back into theboard-view area from thedetail-view area of the lecture room. It is again clear that the PNROOM2 is sound for every one of its input markings Mi.PNROOM that models all the main functionalities of the audiovisual lecture room is then the PNROOM =ROOM1.P1 ROOM2 that is also sound according to Lemma 6.Design and implementation of the programming systems that accept the messages generated by the area sensors of the audiovisual lecture room (these messages are represented by the tokens1–6 in the resulting PN) and that realize the automatic switching of the camera systems and the automatic editing functionality during recordings of presentations are represented by the ANCAM1 in Figure 15. The input place IP3 of the ANCAM1 accepts all the messages represented by the tokens 1–6 and generated by the area sensors of the audiovisual lecture room. Resource place R20 with the token 0 of the only one allowed static marking Ms of this AN (this static marking Ms is such the only-one element of the set Ms of the ANCAM1) represents the critical section mechanism of the whole programming system. This critical section guarantees that at most one message will be serviced by the programming system at the given time. The place P2 then represents the algorithm which realizes the automatic switching of the camera systems. The firing of the output transition OT3 then discards every accepted message from the given area sensor. It is again clear that the ANCAM1 is sound for every one of its input markings Mi.Figure 15
SNT agent netCAM1.Figure16 shows the resulting PNRNET1  that is composed of the PNROOM =ROOM1.P1 ROOM2 and the ANCAM1 using theASYNC-PROC operator such thatRNET1 =ROOM.T1.T3.T10.T11.T12.T13.T14 -CAM1. The PNRNET1 introduces the mechanism of the messages generated by the area sensors of the audiovisual lecture room processing (these messages are represented by the tokens 1–6 in the PNRNET1). The whole PNRNET1 is again sound according to Lemma 13.Figure 16
SNT process netRNET1.The first inner part of the programming systems that accepts the messages generated by the area sensors of the audiovisual lecture room is modeled by the PNCAM2 in Figure 17. Every token of the actual static marking Ms of the only one resource place R30 of this PN represents the speakers that are actually presenting in thegeneral-view,board-view, ordetail-view areas at the given time. Every (anonymous) speaker that is presenting in thegeneral-view,board-view,detail-view areas, respectively, at the given time is then modeled by the tokens 1, 2, and 3, respectively, in the actual static marking Ms of the resource place R30. The set of all the allowed resource markings of this PN is then RMs={(i′1+j′2+k′3)∣i∈N0,j∈N0,k∈N0}. The functionalities of the PNCAM2 are as in the following:(i)
Acceptance of the message1 (entry of the speaker into thegeneral-view area from the nonscanned area of the lecture room) results in the firing of the transition T33 and adding of the token 1 (entry of the speaker into thegeneral-view area) into the resource place R30.(ii)
Acceptance of the message3 (exit of the speaker outside thegeneral-view area and entry of this speaker into theboard-view area) results in the firing of the transition T32, removing the token 1 (exit of the speaker outside thegeneral-view area) from the resource place R30 and adding the token 2 (entry of the speaker into theboard-view area) into the resource place R30.(iii)
Acceptance of the message5 (exit of the speaker outside theboard-view area and entry of this speaker into thedetail-view area) results in the firing of the transition T32, removing of the token 2 (exit of the speaker outside theboard-view area) from the resource place R30, and adding of the token 3 (entry of the speaker into thedetail-view area) into the resource place R30.(iv)
Acceptance of the message2 (exit of the speaker outside thegeneral-view area into the nonscanned area of the lecture room) results in the firing of the transition T32 and removing of the token 1 (exit of the speaker outside thegeneral-view area into the nonscanned area) from the resource place R30. If the resource place R30 still contains at least one token 1 (i.e., at least one speaker is still presented in thegeneral-view area) the transition T35 then fires and the token 2 is changed into the token 0 (i.e., no camera switching will be performed). The transition T34 will fire otherwise and the camera switching can be performed.(v)
Acceptance of the message4 (exit of the speaker outside theboard-view area and entry of this speaker into thegeneral-view area) results in the firing of the transition T31, removing of the token 2 (exit of the speaker outside theboard-view area) from the resource place R30 and adding of the token 1 (entry of this speaker into thegeneral-view area) into the resource place R30. If the resource place R30 still contains at least one token 2 (i.e., at least one speaker is still presented in theboard-view area) the transition T35 then fires and the token 4 is changed into the token 0 (i.e., no camera switching will be performed). The transition T34 will fire otherwise and the camera switching can be performed.(vi)
Acceptance of the message6 (exit of the speaker outside thedetail-view area and entry of this speaker into theboard-view area) results in the firing of the transition T31, removing of the token 3 (exit of the speaker outside thedetail-view area) from the resource place R30, and adding of the token 2 (entry of this speaker into theboard-view area) into the resource place R30. If the resource place R30 still contains at least one token 3 (i.e., at least one speaker is still presented in thedetail-view area) the transition T35 then fires and the token 6 is changed into the token 0 (i.e., no camera switching will be performed). The transition T34 will fire otherwise and the camera switching can be performed.(vii)
The transition T35 will fire otherwise and no camera switching will be performed.Figure 17
SNT process netCAM2.It is not difficult to prove that the whole PNCAM2 is sound for every one of its input markings Mi.The second inner part of the programming systems that accepts the messages generated by the area sensors of the audiovisual lecture room is modeled by the PNCAM3 in Figure 18. Every token of the actual static marking Ms of the only one resource place R40 of this PN represents the actual state of the cameras for thegeneral-view,board-view, ordetail-view areas, such that(i)
the token0 represents the state where all the three cameras are nonactive,(ii)
the token1 represents the state where only the shot for thegeneral-view area is actively scanned and all of the remaining cameras are nonactive,(iii)
the token2 represents the state where only the shot for theboard-view area is actively scanned and all of the remaining cameras are nonactive,(iv)
the token3 represents the state where only the shot for thedetail-view area is actively scanned and all of the remaining cameras are nonactive.Figure 18
SNT process netCAM3.The set of allowed resource markings of this PN is thenRMs=k∣k∈0,1,2,3. The functionalities of the PNCAM2 are as in the following:(i)
Acceptance of the message1 (entry of the speaker into thegeneral-view area from the nonscanned area of the lecture room) results in the firing of the transition T42 only if all the three cameras are in nonactive states (i.e., the token 0 is actually presented in the marking of the resource place R40) and the token 1 will be then added into the resource place R40 (i.e., only the camera for thegeneral-view area is in active state and all of the remaining cameras are in nonactive states), otherwise the transition T46 will fire and the actual states of all the cameras will be unchanged,(ii)
Acceptance of the message2 (exit of the speaker from thegeneral-view area and entry into the nonscanned area of the lecture room) results in the firing of the transition T43 if only the camera for thegeneral-view area is in active state and all of the remaining cameras are in nonactive states (i.e., the token 1 is actually presented in the marking of the resource place R40) and the token 0 will be then added into the resource place R40 (i.e., all the cameras are in nonactive states), otherwise the transition T46 will fire and the actual states of all the cameras will be unchanged,(iii)
… and similarly for the acceptance of the messages3–6.It is again clear that the PNCAM3 is sound for every one of its input markings Mi.We will then construct the resulting PNRNET with the support of the PLACE-SUBST operator applications such that (6)RNET=RNET1.P20CAM2.OP4CAM3,where RNET1=ROOM.T1.T3.T10.T11.T12.T13.T14-CAM1 and ROOM=ROOM1.P1ROOM2; that is, (7)
R
N
E
T
=
R
O
O
M
1
.
P
1
R
O
O
M
2
.
T
1
.
T
3
.
T
10
.
T
11
.
T
12
.
T
13
.
T
14
-
C
A
M
1
.
P
20
C
A
M
2
.
O
P
4
C
A
M
3
.The resulting PNRNET is also sound according to Lemmas 6 and 13.


## 4. Conclusions

Design and implementation of the programming systems which realize the automatic switching of the camera systems and the automatic editing functionality during recordings of presentations in the audiovisual lecture room involved the use of the SNT Petri process and agent nets formal theory. The simplified SNTPAN model of the given system is shown in Figures14–18 (a more detailed model is much more complicated and its design used the theory of the timed SNTPANs [18]).There is an opportunity to define additional operators for the class of SNTPANs and to generalize it (for instance, the SYNC-PROC composition operator that models synchronous nonrecursive calling of chosen method represented by a PNPN2 of some programming system from the body of another method of the same programming system represented by a PN PN1). Selected PN or AN then represents typically a method in the model of the programming system realized with the support of the SNTPAN formalism.At the Faculty of Economics, VŠB-Technical University of Ostrava, the recordings of presentations were realized with the support of highly mentioned lecture room with the automated editing. The rich-media recordings were published through theMediaInTouch programming system that is also integrated with the LMS systemMoodle in the present time. This integration is based on the presence of the accessibility of theMediaInTouch application programming interface based on the web services technology. Thus it is possible to enable (i.e., insert or share) the recordings of presentations from theMediaInTouch repository as the organic part of every eLearning course content in theMoodle environment. The recordings are such then also the parts of the study materials for the mentioned subjects in the Bachelor and Master studies in theMoodle environment.The lecture room with the support of automated editing enablesall-day fully automated realization of all presentation recordings in the present time. There is then significant financial, personal, and time cost reduction joined with the creation and management of rich-media learning objects in comparison of the usual ways of recording. There is also verifiable improvement of the study results of the students (and particularly of the students with special needs) in the context of the availability of the presentation recordings and their accessibility online or on-demand as the standard part of the virtual university resources.Those technologies can be also crucially beneficial during qualitative extension of provided services for the students with special needs, mainly at the establishment of “barrier-free” information access to recordings of presentations adapted to needs mainly for students with locomotive, visual aural disability while using internationally valid standards.EduArt andMediaInTouch programming systems are also extensively applied at the practical application of the methodology of adaptation of existing and newly created learning objects which are adapted for students with special needs. The main results achieved in this area currently involve(i)
technical solution of the parallel recording of translation of the lecturer into the sign language and text form. The programming implementation of the stated feature is based on the addition of next video stream containing translation of the lecturer into sign language or text form in the resulting record and their synchronizing with performed presentation,(ii)
the transcription of standard eLearning text study supports in the audio form and their availability obtained via podcasting as a part of the MERLINGO portal services,(iii)
automated transcription of spoken text of the lecture recorded by the recording and assistance service into the written text.



---

*Source: 303705-2015-07-14.xml*