Sharif Digital Repository

Nowadays developing autonomous systems, which can act in various environments and interactively perform their assigned tasks, are intensively desirable. These systems would be ready to be applied in different fields such as medicine, controller robots and social life. Reinforcement learning is an attractive area of machine learning which addresses these concerns. In large scales, learning performance of an agent can be improved by using hierarchical Reinforcement Learning techniques and temporary extended actions. The higher level of abstraction helps the learning agent approach lifelong learning goals. In this paper a new method is presented for discovering subgoal states and constructing... 

Rebeca is a recently introduced actor-based language, for modeling concurrent and distributed systems. In this paper, we present our work on model checking Rebeca code. Rebeca is a high level language, comparing to the most of languages used for modeling, in the existing model checker tools. So, we need specific abstraction techniques for model checking Rebeca code. Here, we show some of these abstraction techniques used and some case studies  

Actor-based modeling, with encapsulated active objects which communicate asynchronously, is generally recognized to be well-suited for representing concurrent and distributed systems. In this paper we discuss the actor-based language Rebeca which is based on a formal operational interpretation of the actor model. Its Java-like syntax and object-based style of modeling makes it easy to use for software engineers, and its independent objects as units of concurrency leads to natural abstraction techniques necessary for model checking. We present a front-end tool for translating Rebeca to the languages of existing model checkers in order to model check Rebeca models. Automated modular... 

Rebeca is an actor-based language for modeling concurrent and distributed systems. Its Java-like syntax makes it easy-to-use for practitioners and its formal foundation is a basis to make different formal verification approaches applicable. Compositional verification and abstraction techniques are used in formal verification of Rebeca models to overcome state explosion problems. The main contribution of this paper is to show how model checking and deduction are integrated for verifying certain properties of these models. Deduction is used to prove that abstraction techniques preserve a set of behavioral specifications in temporal logic and is also used in applying the compositional... 

The importance of traffic pattern prediction for traffic management systems has significantly increased in recent years. This paper presents a novel method to find unusual traffic patterns by using topic modeling. We have employed topic models to provide an abstraction of speed camera data from Tehran, the capital of Iran. In this methodology, topic modeling is applied to days of weeks and months in a year and extracts weekly and monthly traffic patterns. Analysis of the abstract descriptions and their adaptation to actual urban traffic patterns prove the effectiveness of the proposed method. The model training convergence is also practically verified. Based on our experiments, our method... 

As contemporary digital systems specifically embedded systems become more and more complex, taking advantage of system-level design is being more widespread. Many embedded systems must operate under strict timing constraints. One of the best methods for examining timing constraints in an embedded system can be done via the performance verification. In this paper an assertion-based verification methodology has been proposed for verifying system-level timing constraints in an embedded system. Performance assertions are specified by an assertion language at the transaction-level of abstraction. A Turing machine and a structure named performance evaluator have been coupled to provide a... 

The importance of traffic pattern prediction for traffic management systems has significantly increased in recent years. This paper presents a novel method to find unusual traffic patterns by using topic modeling. We have employed topic models to provide an abstraction of speed camera data from Tehran, the capital of Iran. In this methodology, topic modeling is applied to days of weeks and months in a year and extracts weekly and monthly traffic patterns. Analysis of the abstract descriptions and their adaptation to actual urban traffic patterns prove the effectiveness of the proposed method. The model training convergence is also practically verified. Based on our experiments, our method... 

The cation radicals of DNA constituents generated by the ionizing radiation initiate the alteration of the bases, which is one main type of cytotoxic DNA lesions. These cation radical spices are known for their role in producing nucleic acid strand break, and it is important to identify the cation radical formation at particular atomic site in these molecules so that the major pathway for the nucleic acid damage may be trapped. In the present study, we explored theoretically energetic, structural, and electronic properties of the possible radicals formed via proton atom abstraction at various sites of sugar part of deoxycytidine cation radical by employing density functional theory at... 

In this paper, we explore theoretically energetic and structural properties of the possible cations formed via hydride ion abstraction at various sites of sugar part of cytosine nucleosides by employing B3LYP exchange-correlation functional with 6-311++G (d,p) orbital basis sets. In general, the hydride ion abstracted sugar cations of cytosine nucleosides have the following stability sequence: caH2′ > caH1′ > caH3′ > caH4′ > caH5′ for cytidine and caH1′ > caH4′ > caH3′ > caH5′ > caH2′ for deoxycytidine. Furthermore, the effect of solvent environment on the stability order of cations integral equation formalism of the polarized model (IEF-PCM) was employed to model aqueous solution. The... 

Abstraction of hydrogen atom from DNA and RNA subunits leads to formation of a neutral radical. The formation of these radicals can lead to harmful structural alternations and formation of multiple lesions in helixes of DNA and RNA. In the present work, we explore theoretically energetic and structural properties of the possible radicals formed via hydrogen atom abstraction at various sites of sugar part of cytosine nucleosides by employing B3LYP exchange-correlation functional with 6-311++G (d,p) orbital basis sets. Two types of free radicals may be found by hydrogen abstraction of sugar part of cytosine nucleosides: carbon centered radicals and the oxygen centered radicals. The computation... 

In this paper, we consider the problem of simulating one copy of a zero-capacity two-way channel from arbitrary many copies of another two-way channel. The motivation for this problem comes from foundation of quantum physics where zero-capacity two-way channels (a.k.a. no-signaling boxes) serve as the abstract objects for studying non-locality. We provide necessary conditions for the possibility of channel simulation using two measures of correlation, namely maximal correlation and hypercontractivity ribbon. It is shown that when these measures are defined appropriately for two-way channels, they are monotonically decreasing under local operations. Our result allows us to establish a... 

In this study, the performance of virtual cut-through switching in the cube-based OTIS architecture, an optoelectronic interconnection architecture for multicomputer systems, is empirically analyzed. Deadlock-free deterministic and adaptive minimal path routing algorithms for this architecture are introduced, and the effects of different network and traffic parameters on average message latency are investigated. This analysis presents a relatively more realistic view of the OTIS architecture than that presented in previous work by considering issues related to a lower level of abstraction (the routing and switching of messages). Among other results, the analysis indicates that depending on... 

Since Di Gianantonio introduced his semantics for exact real number computation, there has always been a struggle to maintain data abstraction and efficiency as much as possible. The interval domain model - or its variations - can be regarded as the standard setting to obtain maximum data abstraction. As for efficiency there has been much focus on sequentially to the extent that these two terms have become almost synonymous. [2, 3] demonstrated that there is not much one can get by sequential computation in the interval domain model. In [4, 5] we reinforced this result by exposing the limited power of (some extensions of) the sequential fragment of Real-PCF. The previous argument suggests... 

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their correctness. In this paper, we develop an actor-based model for describing such systems, use temporal logic to specify properties of the model, and apply different abstraction and verification methods for verifying that the model meets its specification. We use a compositional verification approach for verifying safety properties of these models. For that we introduce a notion of component, based on an user-defined decomposition of the model.... 

In this paper, we present a spatio-temporal event-based approach to video signal analysis and abstraction employing wavelet transform features. The video signal is assumed to be a sequence of overlapping independent visual components called events, which typically are temporally overlapping compact functions that describe temporal evolution of a given set of the spatial parameters of the video signal. We utilize event-based temporal decomposition technique to resolve the overlapping arrangement of the video signal that is known to be one of the main concerns in video analysis via conventional frame-based schemes. In our method, a set of spatial parameters, extracted from the video, is... 

In this article, we solve the problem of minimizing the difference of dual functions of two coradiant functions. We do this by applying a type of duality, that is used in microeconomic theory. Indeed, the dual function of a co-radiant function is decreasing and inverse coradiant. So, we first give various characterizations for the maximal elements of the support sets of this class of functions. Next, by using these results, we obtain the necessary and sufficient conditions for the global minimizers of the difference of two decreasing and inverse coradiant functions. Finally, as an application, we present the necessary and sufficient conditions for the global minimizers of the difference of... 

We provide a detailed review of existing object-oriented software development methodologies, focusing on their development processes. The review aims at laying bare their core philosophies, processes, and internal activities. This is done by using a process-centered template for summarizing the methodologies, highlighting the activities prescribed in the methodology while describing the modeling languages used (mainly diagrams and tables) as secondary to the activities. The descriptions produced using this template aim not to offer a critique on the methodologies and processes, but instead provide an abstract and structured description in a way that facilitates their elaborate analysis for... 

In this paper, we propose extended Rebeca as a tool-supported actor-based language for modeling and verifying concurrent and distributed systems. We enrich Rebeca with a formal concept of components which integrates the message-driven computational model of actor-based languages with synchronous message passing. Components are used to encapsulate a set of internal active objects which react asynchronously to messages by means of methods and which additionally interact via a synchronous message passing mechanism. Components themselves interact only via asynchronous and anonymous messages. We present our compositional verification approach and abstraction techniques, and the theory...