Showing 1–9 of 9 results for author: Jaksic, S

On the iterates of the Laguerre operator

Authors: Smiljana Jakšić, Stevan Pilipović, Nenad Teofanov, Đorđe Vučković

Abstract: We use the iterates of the Laguerre operator to introduce Pilipović spaces on positive orthants. It is shown that such spaces coincide with $G-$type spaces $g_α^α(\mathbb{R}^d_+)$ and $G_α^α(\mathbb{R}^d_+)$, when $α> 1$, and $α\geq 1$, respectively. However, in contrast to $G$-type spaces, Pilipović spaces on positive orthants are nontrivial below the critical index $α= 1$. We also remark that th… ▽ More We use the iterates of the Laguerre operator to introduce Pilipović spaces on positive orthants. It is shown that such spaces coincide with $G-$type spaces $g_α^α(\mathbb{R}^d_+)$ and $G_α^α(\mathbb{R}^d_+)$, when $α> 1$, and $α\geq 1$, respectively. However, in contrast to $G$-type spaces, Pilipović spaces on positive orthants are nontrivial below the critical index $α= 1$. We also remark that there is a natural isomorphism between subspaces of Pilipović spaces on $\mathbb{R}^d$ consisting of even functions, and Pilipović spaces on positive orthants. △ Less

Submitted 17 May, 2024; originally announced May 2024.

MSC Class: 46F05; 33C45

The affine ensemble: determinantal point processes associated with the ax+b group

Authors: Luis Daniel Abreu, Peter Balazs, Smiljana Jakšić

Abstract: We introduce the affine ensemble, a class of determinantal point processes (DPP) in the half-plane C^+ associated with the ax+b (affine) group, depending on an admissible Hardy function ψ. We obtain the asymptotic behavior of the variance, the exact value of the asymptotic constant, and non-asymptotic upper and lower bounds for the variance on a compact set Ω contained in C^+. As a special case on… ▽ More We introduce the affine ensemble, a class of determinantal point processes (DPP) in the half-plane C^+ associated with the ax+b (affine) group, depending on an admissible Hardy function ψ. We obtain the asymptotic behavior of the variance, the exact value of the asymptotic constant, and non-asymptotic upper and lower bounds for the variance on a compact set Ω contained in C^+. As a special case one recovers the DPP related to the weighted Bergman kernel. When ψ is chosen within a finite family whose Fourier transform are Laguerre functions, we obtain the DPP associated to hyperbolic Landau levels, the eigenspaces of the finite spectrum of the Maass Laplacian with a magnetic field. △ Less

Submitted 15 October, 2022; originally announced October 2022.

Comments: 15 pages; J. Math. Soc. Japan, in press

Model-Free Reinforcement Learning for Symbolic Automata-encoded Objectives

Authors: Anand Balakrishnan, Stefan Jakšić, Edgar A. Aguilar, Dejan Ničković, Jyotirmoy V. Deshmukh

Abstract: Reinforcement learning (RL) is a popular approach for robotic path planning in uncertain environments. However, the control policies trained for an RL agent crucially depend on user-defined, state-based reward functions. Poorly designed rewards can lead to policies that do get maximal rewards but fail to satisfy desired task objectives or are unsafe. There are several examples of the use of formal… ▽ More Reinforcement learning (RL) is a popular approach for robotic path planning in uncertain environments. However, the control policies trained for an RL agent crucially depend on user-defined, state-based reward functions. Poorly designed rewards can lead to policies that do get maximal rewards but fail to satisfy desired task objectives or are unsafe. There are several examples of the use of formal languages such as temporal logics and automata to specify high-level task specifications for robots (in lieu of Markovian rewards). Recent efforts have focused on inferring state-based rewards from formal specifications; here, the goal is to provide (probabilistic) guarantees that the policy learned using RL (with the inferred rewards) satisfies the high-level formal specification. A key drawback of several of these techniques is that the rewards that they infer are sparse: the agent receives positive rewards only upon completion of the task and no rewards otherwise. This naturally leads to poor convergence properties and high variance during RL. In this work, we propose using formal specifications in the form of symbolic automata: these serve as a generalization of both bounded-time temporal logic-based specifications as well as automata. Furthermore, our use of symbolic automata allows us to define non-sparse potential-based rewards which empirically shape the reward surface, leading to better convergence during RL. We also show that our potential-based rewarding strategy still allows us to obtain the policy that maximizes the satisfaction of the given specification. △ Less

Submitted 24 February, 2022; v1 submitted 4 February, 2022; originally announced February 2022.

An Algebraic Framework for Runtime Verification

Authors: Stefan Jaksic, Ezio Bartocci, Radu Grosu, Dejan Nickovic

Abstract: Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPS). By measuring how robustly a CPS run satisfies a specification, RV allows in addition, to quantify the resiliency of a CPS to perturbations. In this paper we propose Algebraic Runtime Verification (ARV), a general, semantic framework fo… ▽ More Runtime verification (RV) is a pragmatic and scalable, yet rigorous technique, to assess the correctness of complex systems, including cyber-physical systems (CPS). By measuring how robustly a CPS run satisfies a specification, RV allows in addition, to quantify the resiliency of a CPS to perturbations. In this paper we propose Algebraic Runtime Verification (ARV), a general, semantic framework for RV, which takes advantage of the monoidal structure of runs (w.r.t. concatenation) and the semiring structure of a specification automaton (w.r.t. choice and concatenation), to compute in an incremental and application specific fashion the resiliency measure. This allows us to expose the core aspects of RV, by develo** an abstract monitoring algorithm, and to strengthen and unify the various qualitative and quantitative approaches to RV, by instantiating choice and concatenation with real-valued functions as dictated by the application. We demonstrate the power and effectiveness of our framework on two case studies from the automotive domain. △ Less

Submitted 11 February, 2018; originally announced February 2018.

$G$-type Spaces of Ultradistributions over $\mathbb{R}^d_+$ and the Weyl Pseudo-differential Operators with Radial Symbols

Authors: Smiljana Jaksić, Stevan Pilipović, Bojan Prangoski

Abstract: The first part of the paper is devoted to the $G$-type spaces i.e. the spaces $G^α_α(\mathbb R^d_+)$, $α\geq 1$ and their duals which can be described as analogous to the Gelfand-Shilov spaces and their duals but with completely new justification of obtained results. The Laguerre type expansions of the elements in $G^α_α(\mathbb R^d_+)$, $α\geq 1$ and their duals characterise these spaces through… ▽ More The first part of the paper is devoted to the $G$-type spaces i.e. the spaces $G^α_α(\mathbb R^d_+)$, $α\geq 1$ and their duals which can be described as analogous to the Gelfand-Shilov spaces and their duals but with completely new justification of obtained results. The Laguerre type expansions of the elements in $G^α_α(\mathbb R^d_+)$, $α\geq 1$ and their duals characterise these spaces through the exponential and sub-exponential growth of coefficients. We provide the full topological description and by the nuclearity of $G_α^α(\mathbb{R}^d_+)$, $α\geq 1$ the kernel theorem is proved. The second part is devoted to the class of the Weyl operators with radial symbols belonging to the $G$-type spaces. The continuity properties of this class of pseudo-differential operators over the Gelfand-Shilov type spaces and their duals are proved. In this way the class of the Weyl pseudo-differential operators is extended to the one with the radial symbols with the exponential and sub-exponential growth rate. △ Less

Submitted 12 February, 2016; originally announced February 2016.

Extension theorem of Whitney type for $\mathcal S(\mathbb{R}_+^d)$ by the use of the Kernel Theorem

Authors: Smiljana Jaksić, Bojan Prangoski

Abstract: We study the expansions of the elements in $\mathcal S(\mathbb{R}_+^d)$ and $\mathcal{S}'(\mathbb{R}_+^d)$ with respect to the Laguerre orthonormal basis, extending the result of M. Guillemont-Teissier in the case $d=1$. As a consequence, we obtain the Schwartz kernel theorem for $\mathcal{S}(\mathbb{R}_+^d)$ and $\mathcal{S}'(\mathbb{R}_+^d)$ and the extension theorem of Whitney type for… ▽ More We study the expansions of the elements in $\mathcal S(\mathbb{R}_+^d)$ and $\mathcal{S}'(\mathbb{R}_+^d)$ with respect to the Laguerre orthonormal basis, extending the result of M. Guillemont-Teissier in the case $d=1$. As a consequence, we obtain the Schwartz kernel theorem for $\mathcal{S}(\mathbb{R}_+^d)$ and $\mathcal{S}'(\mathbb{R}_+^d)$ and the extension theorem of Whitney type for $\mathcal{S}(\mathbb{R}_+^d)$. △ Less

Submitted 12 February, 2016; originally announced February 2016.

A Typed Model for Dynamic Authorizations

Authors: Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Jorge A. Pérez, Hugo Torres Vieira

Abstract: Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to e… ▽ More Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to enrich communication-based systems with authorization specification and delegation; here authorizations regard channel usage and delegation refers to the act of yielding an authorization to another party. Our model includes: (i) a novel sco** construct for authorization, which allows to specify authorization boundaries, and (ii) communication primitives for authorizations, which allow to pass around authorizations to act on a given channel. An authorization error may consist in, e.g., performing an action along a name which is not under an appropriate authorization scope. We introduce a ty** discipline that ensures that processes never reduce to authorization errors, even when authorizations are dynamically delegated. △ Less

Submitted 10 February, 2016; originally announced February 2016.

Comments: In Proceedings PLACES 2015, arXiv:1602.03254

Journal ref: EPTCS 203, 2016, pp. 73-84

Precise subty** for synchronous multiparty sessions

Authors: Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Nobuko Yoshida

Abstract: The notion of subty** has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subty**, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with r… ▽ More The notion of subty** has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subty**, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subty** for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness. △ Less

Submitted 10 February, 2016; originally announced February 2016.

Comments: In Proceedings PLACES 2015, arXiv:1602.03254

ACM Class: D.3.3; F.3.2

Journal ref: EPTCS 203, 2016, pp. 29-43

Dynamic Role Authorization in Multiparty Conversations

Authors: Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Jorge A. Pérez, Hugo Torres Vieira

Abstract: Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at ru… ▽ More Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at runtime. Building on previous work on conversation types with flexible role assignment, here we report initial results on a typed framework for the analysis of multiparty communications with dynamic role authorization and delegation. In the underlying process model, communication prefixes are annotated with role authorizations and authorizations can be passed around. We extend the conversation type system so as to statically distinguish processes that never incur in authorization errors. The proposed static discipline guarantees that processes are always authorized to communicate on behalf of an intended role, also covering the case in which authorizations are dynamically passed around in messages. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: In Proceedings BEAT 2014, arXiv:1408.5564

ACM Class: D.3.1; F.3.2

Journal ref: EPTCS 162, 2014, pp. 1-8