Статья содержит отчет по проведении 8-й Российской летней школы по информационному поиску (The 8th Russian Summer School in Information Retrieval (RuSSIR 2014)).
В статье приведен отчет о проведении 9-ой Российской летней школы по информационному поиску 9th Russian Summer School in Information Retrieval (RuSSIR 2015).
We propose an accelerated gradient-free method with a non-Euclidean proximal operator associated with the p-norm (1 ⩽ p ⩽ 2). We obtain estimates for the rate of convergence of the method under low noise arising in the calculation of the function value. We present the results of computational experiments.
Checking the correctness of distributed systems is one of the most difficult and urgent problems in software engineering. A combined toolset for the verification of real-time distributed systems (RTDS) is described. RTDSs are specified as statecharts in the Universal Modeling Language (UML). The semantics of statecharts is defined by means of hierarchical timed automata. The combined toolset consists of a UML statechart editor, a verification tool for model checking networks of real-time automata in UPPAAL, and a translator of UML statecharts into networks of timed automata. The focus is on the translation algorithm from UML statecharts into networks of hierarchical timed automata. To illustrate the proposed approach to the verification of RTDSs, a toy example of a real-time crossroad traffic control system is analyzed.
We design temporal description logics (TDLs) suitable for reasoning about temporal conceptual data models and investigate their computational complexity. Our formalisms are based on DL-Lite logics with three types of concept inclusions (ranging from atomic concept inclusions and disjointness to the full Booleans), as well as cardinality constraints and role inclusions. The logics are interpreted over the Cartesian products of object domains and the flow of time (ℤ, <), satisfying the constant domain assumption. Concept and role inclusions of the TBox hold at all moments of time (globally), and data assertions of the ABox hold at specified moments of time. To express temporal constraints of conceptual data models, the languages are equipped with flexible and rigid roles, standard future and past temporal operators on concepts, and operators “always” and “sometime” on roles. The most expressive of our TDLs (which can capture lifespan cardinalities and either qualitative or quantitative evolution constraints) turns out to be undecidable. However, by omitting some of the temporal operators on concepts/roles or by restricting the form of concept inclusions, we construct logics whose complexity ranges between NLogSpace and PSpace. These positive results are obtained by reduction to various clausal fragments of propositional temporal logic, which opens a way to employ propositional or first-order temporal provers for reasoning about temporal data models.