Informacja

Drogi użytkowniku, aplikacja do prawidłowego działania wymaga obsługi JavaScript. Proszę włącz obsługę JavaScript w Twojej przeglądarce.

English (EN)·Polski (PL)·Yкраїнський (UK)
Przejdź do strony domowej biblioteki Centralna Biblioteka Wojskowa Link otwiera się w nowym oknie Logo biblioteki Prolib Integro - strona głównaCentralna Biblioteka Wojskowa

Wyszukujesz frazę "temporal logic" wg kryterium: Temat

  Lista filtrów
Wyrównaj
    Wyświetlanie 1-23 z 23
    Tytuł:
    Siła i słabość logik modalnych
    The Strengths and Weaknesses of Modal Logics
    Autorzy:
    Czakon, Marcin
    Powiązania:
    https://bibliotekanauki.pl/articles/909495.pdf
    Data publikacji:
    2020-03-31
    Wydawca:
    Uniwersytet Warszawski. Wydział Filozofii
    Tematy:
    modal logic
    temporal logic
    epistemic logic
    Opis:
    This is a review of the book Jedność i wielość logik modalnych (The Unity and Diversity of Modal Logics) edited by Marcin Tkaczyk. The book contains discussions of the most recent results of contemporary modal logic, focusing on regular modal logics, epistemic logic, and temporal logic. The book comprises four chapter, each of which deals with selected formal-logical and philosophical problems associated with modal logic.
    Źródło:
    Filozofia Nauki; 2020, 28, 1; 125-132
    1230-6894
    2657-5868
    Pojawia się w:
    Filozofia Nauki
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
    Autorzy:
    Indrzejczak, Andrzej
    Powiązania:
    https://bibliotekanauki.pl/articles/749932.pdf
    Data publikacji:
    2017
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Tematy:
    temporal logic
    linear time
    hypersequent calculus
    cut elimination
    Opis:
    Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.
    Źródło:
    Bulletin of the Section of Logic; 2017, 46, 1/2
    0138-0680
    2449-836X
    Pojawia się w:
    Bulletin of the Section of Logic
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Zmienna czasowa w starożytnej i średniowiecznej teorii zdań warunkowych
    Time Variable in Ancient and Medieval Concepts of the Conditional
    Autorzy:
    Tkaczyk, Marcin
    Powiązania:
    https://bibliotekanauki.pl/articles/2013333.pdf
    Data publikacji:
    2007
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    zdanie warunkowe
    implikacja
    consequentia
    logika temporalna
    conditional
    implication
    temporal logic
    Opis:
    A problem of mutual relationships of the concepts of the conditional by Diodorus Cronus, Philo, Abelard, Pseudo Scotus (Iohannes do Cornubia?) and William of Ockham is examined. Both in ancient and medieval logic there seems to be a discussion on a version of the concept that involves a time variable and one that does not. Diodorus, Pseudo Scotus and Ockham, when defining the conditional, make essential use of temporal concepts, while Philo and Abelard do not. It is discussed, which concepts examined may be identified with one another and what is the rôle that the temporal concepts play.
    Źródło:
    Roczniki Filozoficzne; 2007, 55, 2; 99-121
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Useful Four-Valued Extension of the Temporal Logic KtT4
    Autorzy:
    Degauquier, Vincent
    Powiązania:
    https://bibliotekanauki.pl/articles/749896.pdf
    Data publikacji:
    2018
    Wydawca:
    Uniwersytet Łódzki. Wydawnictwo Uniwersytetu Łódzkiego
    Tematy:
    temporal logic
    many-valued logic
    bi-intuitionistic logic
    paraconsistent logic
    sequent calculus
    duality
    cut-redundancy
    Opis:
    The temporal logic KtT4 is the modal logic obtained from the minimal temporal logic Kt by requiring the accessibility relation to be reflexive (which corresponds to the axiom T) and transitive (which corresponds to the axiom 4). This article aims, firstly, at providing both a model-theoretic and a proof-theoretic characterisation of a four-valued extension of the temporal logic KtT4 and, secondly, at identifying some of the most useful properties of this extension in the context of partial and paraconsistent logics.
    Źródło:
    Bulletin of the Section of Logic; 2018, 47, 1
    0138-0680
    2449-836X
    Pojawia się w:
    Bulletin of the Section of Logic
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Application of deductive reasoning to the verification of archimate behavioral elements
    Autorzy:
    Klimek, Radosław
    Szwed, Piotr
    Jędrusik, Stanisław
    Powiązania:
    https://bibliotekanauki.pl/articles/431909.pdf
    Data publikacji:
    2013
    Wydawca:
    Wydawnictwo Uniwersytetu Ekonomicznego we Wrocławiu
    Tematy:
    Deductive temporal reasoning
    software verification
    ArchiMate
    semantics table¬aux method
    Linear Temporal Logic
    Opis:
    The formal verification of business models has recently become an intensively researched area. It is expected that the application of formal tools may bring such benefits to organizations as the improved quality of products and services and a lower ratio of operational errors. In this paper we discuss the application of a deduction-based method for the verification of the behavioral aspects of ArchiMate models. The first step in our method consists in the translation of the ArchiMate model into Linear Temporal Logic (LTL) formulas. The resulting LTL formulas are then verified to check the expected temporal properties. The verification process is based on the semantics tableaux method and is conducted with an LTL prover. The method is discussed using an example of a business process implemented within a surveillance system.
    Źródło:
    Informatyka Ekonomiczna; 2013, 3(29); 76-97
    1507-3858
    Pojawia się w:
    Informatyka Ekonomiczna
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Geneza niektórych systemów logiki temporalnej
    The Origin of Some Systems of Temporal Logic
    Autorzy:
    Kozanecka-Dymek, Anna
    Powiązania:
    https://bibliotekanauki.pl/articles/2013059.pdf
    Data publikacji:
    2009
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    geneza
    logika temporalna
    zwroty czasowe
    funktory czasowe
    origin
    temporal logic
    tense clauses
    temporal functors
    Opis:
    The article is devoted to the question of the origin of temporal logic. The aim of it is to answer to the question concerning the group of conditions and reasons of constructing such kinds of systems (especially of tense logic and G. H. von Wright’s temporal logic). As a result of conducted considerations, there is stated that there exist two reasons of arising some temporal systems. The first of them was the rebirth of interests of issues involving time in aspect of logic, the second (more essential) – insufficiency of the language of the classical logical calculus to give the formalization of tense clauses. In connection with this there was begun constructing temporal systems providing the linguistic and inferencional apparatus needed to control expressions and inferences containing such clauses. In the article there is also shown how there was led to formalize expressions including various tense clauses, and what follows, to introduce new functors to the language of logic.
    Źródło:
    Roczniki Filozoficzne; 2009, 57, 1; 75-90
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Temporalna interpretacja logiki modalnej
    Temporal Interpretation of Modal Logic
    Autorzy:
    Tkaczyk, Marcin
    Powiązania:
    https://bibliotekanauki.pl/articles/2013148.pdf
    Data publikacji:
    2008
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    logika temporalna
    logika tensalna
    logika modalna
    semantyka relacyjna
    temporal logic
    tense logic
    modal logic
    relational semantics
    Opis:
    Temporal interpretation of modal logic consists in replacing possible worlds with temporal states of the world or any time determinates and the accessibility relation with a relation of passage of time. That issue has been raised by A. N. Prior, who was thinking of propositions as things which could change their truth-values (could become true or become false) with the passage of time. Under such interpretation Prior was reading a formula  as: it (is and) will allways be the case that  or: it (is and) has allways been the case that . The formula  should be read respectively. In the present paper the interpretation in question is examined. Its sources are presented and its consequences are analysed. It is claimed, the interpretation to be highly disputable because of its disagreement with physical meaning of temporal statements, established in the special relativity theory.
    Źródło:
    Roczniki Filozoficzne; 2008, 56, 2; 273-297
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Model Checking Temporal Properties of Reaction Systems
    Weryfikacja temporalnych własności systemów reakcyjnych
    Autorzy:
    Męski, A.
    Penczek, W.
    Rozenberg, G.
    Powiązania:
    https://bibliotekanauki.pl/articles/182724.pdf
    Data publikacji:
    2014
    Wydawca:
    Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
    Tematy:
    reaction systems
    model checking
    temporal logic
    systemy reakcyjne
    weryfikacja modelowa
    logika temporalna
    Opis:
    This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.
    Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.
    Źródło:
    Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2014, 1028; 1-28
    0138-0648
    Pojawia się w:
    Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Logika temporalna w informatyce
    Temporal Logic in Computer Science
    Autorzy:
    Trzęsicki, Kazimierz
    Powiązania:
    https://bibliotekanauki.pl/articles/2012894.pdf
    Data publikacji:
    2010
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    logika
    informatyka
    logika temporalna
    weryfikowanie systemów informatycznych
    logic
    computer science
    temporal logic
    verification of software systems
    Opis:
    Leibniz intended to create a lingua characteristica universalis, a language, in which all knowledge (expressiveness) could be recorded, and a calculus ratiocinator, a method that would make it possible to define in a calculational manner the truth of any sentence in this language. Such an idea is at the basis of contemporary logic. With respect to the correctness of the equipment and of programs such an idea is at the foundations of logical methods of verification of software systems. Today we can see that a further development of informatics indeed depends on the progress of research in logic, and logic – this ancient discipline – has found a rich field for investigations; it has gained new perspectives for studies. Its applications may have a significant practical dimension that philosophers have never dreamed about. 
    Źródło:
    Roczniki Filozoficzne; 2010, 58, 2; 181-205
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Modeling of distributed objects computing pattern combinations using a formal specification language
    Autorzy:
    Taibi, T.
    Ngo, D. C. L.
    Powiązania:
    https://bibliotekanauki.pl/articles/908185.pdf
    Data publikacji:
    2003
    Wydawca:
    Uniwersytet Zielonogórski. Oficyna Wydawnicza
    Tematy:
    informatyka
    Balanced Pattern Specification Language (BPSL)
    First-Order Logic (FOL)
    Temporal Logic of Actions (TLA)
    substitution
    addition
    elimination
    Opis:
    Design patterns help us to respond to the challenges faced while developing Distributed Object Computing (DOC) applications by shifting developers' focus to high-level design concerns, rather than platform specific details. However, due to the inherent ambiguity of the existing textual and graphical descriptions of the design patterns, users are faced with difficulties in understanding when and how to use them. Since design patterns are seldom used in isolation but are usually combined to solve complex problems, the above-mentioned difficulties have even worsened. The formal specification of design patterns and their combination is not meant to replace the existing means of describing patterns, but to complement them in order to achieve accuracy and to allow rigorous reasoning about them. The main problem of the existing formal specification languages for design patterns is the lack of completeness. This is mainly because they tend to focus on specifying either the structural or behavioral aspects of design patterns but not both of them. Moreover, none of them even ventured in specifying DOC patterns and pattern combinations. We propose a simple yet Balanced Pattern Specification Language (BPSL) aimed to achieve equilibrium by specifying both the aspects of design patterns. The language combines two subsets of logic: one from the First-Order Logic (FOL) and the other from the Temporal Logic of Actions (TLA).
    Źródło:
    International Journal of Applied Mathematics and Computer Science; 2003, 13, 2; 239-253
    1641-876X
    2083-8492
    Pojawia się w:
    International Journal of Applied Mathematics and Computer Science
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Weryfikacja modelowa interpretowanych sieci Petriego sterowania
    Model checking of control interpreted Petri Nets
    Autorzy:
    Grobelna, I.
    Powiązania:
    https://bibliotekanauki.pl/articles/152412.pdf
    Data publikacji:
    2011
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    weryfikacja modelowa
    sterownik logiczny
    interpretowane sieci Petriego sterowania
    logika temporalna
    model checking
    logic controller
    control interpreted Petri nets
    temporal logic
    Opis:
    Artykuł przedstawia oryginalne podejście do weryfikacji modelowej interpretowanych sieci Petriego sterowania. Sieci Petriego są powszechnie wykorzystywane w przemyśle. Najczęściej jednak weryfikowane są pod kątem właściwości strukturalnych, a właściwości behawioralne (mimo ich dużego znaczenia) są pomijane. Technika weryfikacji modelowej pozwala na weryfikację właściwości opisujących zachowanie projektowanego systemu. Model logiczny otrzymany na podstawie istniejącej sieci Petriego sterowania przedstawiany jest na poziomie RTL w taki sposób, że nadaje się zarówno do formalnej weryfikacji, jak i do syntezy logicznej jako rekonfigurowalny sterownik logiczny lub PLC.
    The paper introduces a novel approach to model checking with Control Interpreted Petri Nets [15]. Petri Nets [9, 11, 12, 13] are commonly used in the industry. However, they are mostly verified against structural properties, and behavioral properties are out of scope. The model checking technique [3, 7, 8, 21, 22] allows verifying properties which describe behavior of the designed system. Properties to be verified are expressed in temporal logic [16, 17, 18, 19, 20]. The logical model (Fig. 1) derived from existing Petri net is presented at RTL level (Register Transfer Level) in such a way, that it is easy to be formally verified as well as to logical synthesized as a reconfigurable logic controller or PLC (Programmable Logic Controller). It operates on variables which correspond to places, input and output signals of the Control Interpreted Petri Net (Section 3). The variables change their values according to some specified rules. The logical model is afterwards transformed into input format of the NuSMV model checker [23] and formally verified (Section 4). Control Interpreted Petri Net (Fig. 2) is divided into elementary subnets (Fig. 3). Each elementary subnet consists of a single place and its input and output transitions. Each elementary subnet is interpreted as a single segment of model description in the NuSMV tool. Each elementary subnet represents a two-states state machine which is usually realized as a single macrocell (Fig. 4) in the FPGA circuit. The properties to be verified are expressed in LTL or CTL logic. If any of them is not satisfied in the described system model, the appropriate counterexample is generated (Fig. 6). In the example in the paper the verification finds a subtle error resulting from incorrect / incomplete specification (Fig. 5) and allows the user to localize the error source.
    Źródło:
    Pomiary Automatyka Kontrola; 2011, R. 57, nr 6, 6; 666-670
    0032-4140
    Pojawia się w:
    Pomiary Automatyka Kontrola
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    O wyrażalności niektórych relacji czasowych i własności czasu w języku systemów logiki temporalnej G. H. von Wrighta
    On the Expression of Temporal Relations and Properties of Time in the Language of the System of G. H. von Wright’s Temporal Logic
    Autorzy:
    Kozanecka, Anna
    Leszczyńska, Magdalena
    Powiązania:
    https://bibliotekanauki.pl/articles/2013337.pdf
    Data publikacji:
    2007
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    czas
    własności czasowe
    relacje czasowe
    logika temporalna
    And Next
    And Then
    wyrażalność
    adekwatność
    zastosowanie
    time
    temporal properties
    temporal relations
    temporal logic
    expression
    adequacy
    application
    Opis:
    The paper discusses the problems of the expression of some temporal relations and properties of time in the language of the systems of G.H. von Wright’s temporal logic. It seeks to answer the question whether the systems of von Wright’s temporal logic are adequate to express by means of axioms (and theorems) some temporal relations and properties of physical time. What follows, whether they be applied in the natural sciences, mainly in physics. The first part of the paper gives a definition of physical time and briefly discusses its most important properties and temporal relations. The second part of the paper shows a syntactic characterisation of the And Next and And Then systems constructed by von Wright. The third part, the last part of the paper, seeks to answer the above question about the expression of some temporal relations and properties of time in the language of the systems of von Wright’s temporal logic, and how they can be applied in the natural sciences, mainly in physics.
    Źródło:
    Roczniki Filozoficzne; 2007, 55, 2; 43-65
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Weryfikowanie specyfikacji wymagań sterownika logicznego za pomocą diagramów aktywności UML, logiki temporalnej LTL i środowiska NuSMV
    Verification of logic controller requirements specification by means of UML activity diagrams, LTL temporal logic and NuSMV tool
    Autorzy:
    Grobelna, I.
    Grobelny, M.
    Powiązania:
    https://bibliotekanauki.pl/articles/277589.pdf
    Data publikacji:
    2013
    Wydawca:
    Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów
    Tematy:
    diagramy aktywności UML
    specyfikacja
    model logiczny
    weryfikacja modelowa
    logika temporalna
    UML activity diagrams
    specification
    logical model
    model checking
    temporal logic
    Opis:
    W artykule przedstawiono ideę zastosowania diagramów aktywności UML do specyfikacji wymagań dotyczących zachowania sterownika logicznego. Lista wymagań podlegających weryfikacji zwykle definiowana jest bezpośrednio za pomocą formuł logiki temporalnej. Użycie przyjaznych dla użytkownika, powszechnie znanych i wykorzystywanych diagramów pozwala na prostsze i bardziej intuicyjne zapisanie wymagań. Diagramy są następnie formalnie przekształcane do formuł liniowej logiki temporalnej (LTL).
    The article introduces an idea to use UML activity diagrams [1-5] for specification of requirements regarding logic controller behavior. Requirements list to be verified [14] (using model checking technique [6, 7]) is usually directly defined using temporal logic formulas [12, 15]. Using user-friendly, commonly known and practiced diagrams allows to easier and more intuitively write down the requirements easier and more intuitively. Activity diagrams are then formally transformed into linear temporal logic (LTL) formulas. In this paper some sample UML activity diagrams which specify global properties are presented, together with their interpretation using LTL logic. To perform model checking process, model description (based i.e. on a control interpreted Petri net [8] or indirectly on an UML activity diagram [11]), and requirements list are needed. Afterwards it is checked, whether defined properties are satisfied in specified model description. If a requirement cannot be fulfilled, appropriate counterexample is generated allowing to localize error source. The article is structured as follows. Section 1 is an introduction. Background of a logic controller specification and its verification is presented in section 2. A novel approach to logic controller requirements definition using activity diagrams is shown in section 3. The paper ends with a short summary.
    Źródło:
    Pomiary Automatyka Robotyka; 2013, 17, 10; 188-192
    1427-9126
    Pojawia się w:
    Pomiary Automatyka Robotyka
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Towards partial order reductions for fragments of alternating-time temporal logic
    O redukcjach częścio-porządkowych dla fragmentów logiki temporalnej czasu alternatywnego
    Autorzy:
    Dembiński, P.
    Jamroga, W.
    Mazurkiewicz, A.
    Penczek, W.
    Powiązania:
    https://bibliotekanauki.pl/articles/182716.pdf
    Data publikacji:
    2016
    Wydawca:
    Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
    Tematy:
    Alternating-Time Temporal Logic
    asynchronous systems
    partial order reduction
    traces
    logika temporalna czasu alternującego
    systemy asynchroniczne
    redukcje częścio-porządkowe
    ślady
    Opis:
    A general semantics of strategic abilities of agents in asynchronous systems with and without perfect information is proposed, and some general complexity results for verification of strategic abilities in asynchronous systems are presented. A methodology for partial order reduction (POR) in verification of agents with imperfect information is developed, based on the notion of traces introduced by Mazurkiewicz. Two semantics of ATL∗ −X are considered and it is shown that for memoryless imperfect information (|=ir) contrary to memoryless perfect information (|=Ir), one can apply techniques known for LTL−X.
    Raport definiuje ogólną semantykę dla strategicznych umiejętności agentów w systemach asynchronicznych z pełną i częściową informacją, oraz prezentuje ogólne wyniki dotyczące złożoności weryfikacji strategicznych możliwości w systemach asynchronicznych. Metoda redukcji częścio-porządkowych, wykorzystująca ślady Mazurkiewicza, została zastosowana do weryfikacji agentów z niepełną informacją. Dla rozważanych dwóch semantyk logiki ATL*_x zostało pokazane, że dla bezpamięciowej niepełnej informacji (|=ir) w przeciwieństwie do bezpamięciowej pełnej informacji (|=Ir), można zastosować metody znane dla LTL_x.
    Źródło:
    Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2016, 1036; 1-32
    0138-0648
    Pojawia się w:
    Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Ontology-based access to temporal data with Ontop: A framework proposal
    Autorzy:
    Güzel Kalaycı, Elem
    Brandt, Sebastian
    Calvanese, Diego
    Ryzhikov, Vladislav
    Xiao, Guohui
    Zakharyaschev, Michael
    Powiązania:
    https://bibliotekanauki.pl/articles/330542.pdf
    Data publikacji:
    2019
    Wydawca:
    Uniwersytet Zielonogórski. Oficyna Wydawnicza
    Tematy:
    metric temporal logic
    ontology based data access
    SPARQL query
    Ontop platform
    logika temporalna
    baza danych ontologiczna
    język zapytań SPARQL
    platforma Ontop
    Opis:
    Predictive analysis gradually gains importance in industry. For instance, service engineers at Siemens diagnostic centres unveil hidden knowledge in huge amounts of historical sensor data and use it to improve the predictive systems analysing live data. Currently, the analysis is usually done using data-dependent rules that are specific to individual sensors and equipment. This dependence poses significant challenges in rule authoring, reuse, and maintenance by engineers. One solution to this problem is to employ ontology-based data access (OBDA), which provides a conceptual view of data via an ontology. However, classical OBDA systems do not support access to temporal data and reasoning over it. To address this issue, we propose a framework for temporal OBDA. In this framework, we use extended mapping languages to extract information about temporal events in the RDF format, classical ontology and rule languages to reflect static information, as well as a temporal rule language to describe events. We also propose a SPARQL-based query language for retrieving temporal information and, finally, an architecture of system implementation extending the state-of-the-art OBDA platform Ontop.
    Źródło:
    International Journal of Applied Mathematics and Computer Science; 2019, 29, 1; 17-30
    1641-876X
    2083-8492
    Pojawia się w:
    International Journal of Applied Mathematics and Computer Science
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    O rodzajach logik temporalnych
    Autorzy:
    Kozanecka, Anna
    Powiązania:
    https://bibliotekanauki.pl/articles/2013346.pdf
    Data publikacji:
    2007
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    czas gramatyczny
    logika temporalna
    logika czasów gramatycznych
    logika czasu
    And Next – „i następnie”
    And Then – „i wtedy”
    Tense
    Temporal Logic
    Tense Logic
    Logic of Time
    Chronological Logic
    And Next
    And Then
    Opis:
    The article is devoted to the problems of different kinds of logics defined as “temporal” (Temporal Logic). At present the term “temporal logic” is used to denote several mutually independent logical systems containing different specific temporal operators and being used in many different branches of knowledge. The aim of the article is to organize this issue. Parts I, II and III of the article discuss temporal logics that may be used in natural sciences (mainly physics and cosmology): tense logic, also called logic of temporal clauses, logic of time (containing time variable) and von Wright’s systems of temporal logic. In Part IV, the last part of the article, temporal systems are presented that make use of the concept of time in computer programs. Non-standard approaches have been omitted.
    Źródło:
    Roczniki Filozoficzne; 2007, 55, 1; 189-199
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej
    Formal verification of a state machine with use of temporal logic
    Autorzy:
    Grobelna, I.
    Powiązania:
    https://bibliotekanauki.pl/articles/154298.pdf
    Data publikacji:
    2009
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    algorytmiczne maszyny stanów ASM
    logika temporalna
    technika Model Checking
    algorithmic state machines ASM
    temporal logic
    formal verification of specification
    Model Checking technique
    Opis:
    Artykuł przedstawia koncepcję specyfikacji współbieżnego procesu sterowania cyfrowego za pośrednictwem diagramów algorytmicznych maszyn stanów ASM w języku aprobowanym przez profesjonalne narzędzie model checker. Specyfikacja może zostać następnie formalnie zweryfikowana pod kątem wymagań stawianych projektowanemu systemowi. Lista wymagań tworzona jest przy wykorzystaniu liniowej logiki temporalnej LTL. Formalna weryfikacja Model Checking polega na sprawdzeniu, czy model systemu spełnia stawiane mu wymagania. W przypadku wykrycia niespóności generowany jest odpowiedni kontrprzykład.
    The paper presents the formal specification method of concurrent control processes in form of algorithmic state machines ASM [5] in a language accepted by a professional model checker tool NuSMV. Basing on linear temporal logic LTL [7, 8, 9, 16] a requirement list (Fig. 6) for the system model is prepared. Formal verification Model Checking [17, 19] consists in comparison of the model description and the requirements list. If some requirements cannot be fulfilled, the appropriate counterexample is generated (Fig. 7), which allows localizing the error source. The ASM diagrams (Fig. 4) are fully determined, but they do not support modularity, that is why they are not well suited for specification of concurrent controlling processes. The paper includes a short introduction to the theory of algorithmic state machines ASM (Section 2), temporal logic (Section 3) and model checking technique (Section 4). The proposed solution is presented on an example (Section 5) of the process of controlling (partially concurrent) movements of two vehicles (Fig. 2). The formal verification method of the ASM diagrams with its advantages and disadvantages as well as the general conclusions are given at the end of the paper (Section 6).
    Źródło:
    Pomiary Automatyka Kontrola; 2009, R. 55, nr 7, 7; 457-460
    0032-4140
    Pojawia się w:
    Pomiary Automatyka Kontrola
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    From workflow design patterns to logical specifications
    Odwzorowanie wzorców projektowych w specyfikację logiczną systemu
    Autorzy:
    Klimek, R.
    Powiązania:
    https://bibliotekanauki.pl/articles/282120.pdf
    Data publikacji:
    2013
    Wydawca:
    Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
    Tematy:
    formal verification
    temporal logic
    deduction
    semantic tableaux
    design patterns
    generating logical specification
    weryfikacja formalna
    logika temporalna
    dedukcja
    tablice semantyczne
    wzorce projektowe
    generowanie specyfikacji logicznej
    Opis:
    This work concerns issues related to automatic generation of logical specifications. Logical specifications can be extracted directly from developed software models. Received specification can be used in the process of a system formal verification using a deductive approach. The generated logical specification is just a set of temporal logie fonnulas as well as verified system properties are expressed in temporal logie. The extraction process is based on the idea of organizing the whole analyzed model as a set of certain design patterns of control flows. A method of automatic transformation of workflow design patterns to temporal logie formulas is proposed. These formulas constitute a logical specification and may be the first step towards a formal verification of system correctness using any method of the deduction-based reasoning. Applying the presented concepts enables bridging the gap between naturalness and intuitive of the deductive inference and the difficulty of its practical application in the case of software models.
    Praca dotyczy zagadnień związanych z automatyczną generacją i modelowaniem specyfikacji logicznej. Specyfikacja logiczna może być wygenerowana bezpośrednio z modeli oprogramowania. Tak uzyskana specyfikacja następnie może być wykorzystana w procesie formalnej weryfikacji przy wykorzystaniu podejścia dedukcyjnego. Wygenerowana specyfikacja reprezentowana jest przez zbiór formuł logiki temporalnej, również weryfikowane własności systemu mogą i powinny być wyrażone w logice temporalnej. Proces ekstrakcji opiera się na założeniu, aby cały analizowany model oprogramowania został zbudowany w oparciu o przyjęte, dowolne, ale najlepsze dla danej klasy zastosowań, wzorce projektowe. Została zaproponowana metoda automatycznej translacji wzorców projektowych (przepływów) do postaci formuł logiki temporalnej. Formuły te składają się na logiczną specyfikację i mogą stanowić pierwszy krok w kierunku formalnej weryfikacji poprawności systemów z wykorzystaniem dowolnej metody wnioskowania dedukcyjnego. Zastosowanie przedstawionych koncepcji umożliwia połączenie naturalności i intuicyjności samego wnioskowania logicznego oraz praktycznego zastosowania tych metod w przypadku modeli oprogramowania.
    Źródło:
    Automatyka / Automatics; 2013, 17, 1; 59-63
    1429-3447
    2353-0952
    Pojawia się w:
    Automatyka / Automatics
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Formal analysis of use case diagrams
    Formalna analiza diagramów przypadków użycia
    Autorzy:
    Klimek, R.
    Szwed, P.
    Powiązania:
    https://bibliotekanauki.pl/articles/305621.pdf
    Data publikacji:
    2010
    Wydawca:
    Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
    Tematy:
    UML
    przypadek użycia
    model formalny
    weryfikacja
    weryfikacja modelowa
    logika temporalna
    metoda tablic semantycznych
    use case
    formal model
    verification
    model checking
    temporal logic
    semantic tableau
    Opis:
    Use case diagrams play an important role in modeling with UML. Careful modeling is crucial in obtaining a correct and efficient system architecture. The paper refers to the formal analysis of the use case diagrams. A formal model of use cases is proposed and its construction for typical relationships between use cases is described. Two methods of formal analysis and verification are presented. The first one based on a states' exploration represents a model checking approach. The second one refers to the symbolic reasoning using formal methods of temporal logic. Simple but representative example of the use case scenario verification is discussed.
    Diagramy przypadków użycia odgrywają znaczącą rolę w modelowaniu systemów z wykorzystaniem UML. Staranne i dokładne modelowanie ma zasadnicze znaczenie w postępowaniu umożliwiającym uzyskanie poprawnej i efektywnej architektury systemu. Artykuł odnosi się do formalnej analizy diagramów przypadków użycia. Został zaproponowany model formalny przypadku użycia, a także opisano odpowiednie konstrukcje dla relacji występujących pomiędzy przypadkami użycia. Zostały przedstawione dwie formalne metody ich analizy i weryfikacji. Pierwsza oparta jest na eksploracji stanów i reprezentuje podejście nazwane weryfikacją modelową. Druga odwołuje się do wnioskowania symbolicznego z wykorzystaniem logiki temporalnej. Został pokazany prosty i reprezentatywny przykład weryfikacji pewnego scenariusza przypadku użycia.
    Źródło:
    Computer Science; 2010, 11; 115-131
    1508-2806
    2300-7036
    Pojawia się w:
    Computer Science
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Weryfikacja procesów biznesowych metodą dedukcyjną z wykorzystaniem logiki temporalnej
    Deduction-based Formal Verification of Business Models using Temporal Logic
    Autorzy:
    Klimek, R.
    Powiązania:
    https://bibliotekanauki.pl/articles/274553.pdf
    Data publikacji:
    2011
    Wydawca:
    Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów
    Tematy:
    modele biznesowe
    BPMN
    SOA
    wzorce projektowe
    logika temporalna
    wnioskowanie dedukcyjne
    metoda tablic semantycznych
    generowanie specyfikacji
    business models
    workflow design patterns
    temporal logic
    deductive reasoning
    semantic tableaux method
    generating specifications
    Opis:
    Praca dotyczy formalnej analizy i weryfikacji modeli biznesowych wyrażonych w notacji BPMN. Weryfikacja oparta jest na wnioskowaniu dedukcyjnym. Jako metodę wnioskowania dla modeli biznesowych zaproponowano metodę tablic semantycznych, która cechuje się apagogicznością oraz analitycznością. Została przedstawiona metoda translacji podstawowych wzorców projektowych BPMN do formuł logiki temporalnej, stanowiących logiczną specyfikację analizowanegomodelu. Zarówno logiczna specyfikacja, jak i właściwości badanych procesów są wyrażone formułami tzw. najmniejszej logiki temporalnej. Formuły te są następnie przetwarzane z wykorzystaniem metody tablic semantycznych. Innowacyjność proponowanego podejścia może istotnie wpłynąć na redukcję kosztów wytwarzania oprogramowania, ze względu na możliwość wykrycia błędów oprogramowania już w fazie jego modelowania, wyprzedzając tym samym znacznie fazy implementacji i testowania.
    The paper concerns formal analysis and verification of business models expressed in BPMN. This verification is based on a deductive reasoning. As a method of inference for business models semantic tableaux method is proposed. Automatic trans- formations of the basic BPMN workflow patterns to temporal logic formulas are proposed. These formulas constitute a logical specification of the analyzed model. Both the logical specification and the desired system properties are expressed as formulas of the smallest linear temporal logic. These formulas are later processed using semantic tableaux method. Applying this innovative concept might result in software development costs reduction as some errors might be addressed in the modeling phase not in implementation or testing phase.
    Źródło:
    Pomiary Automatyka Robotyka; 2011, 15, 12; 190-193
    1427-9126
    Pojawia się w:
    Pomiary Automatyka Robotyka
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    A system for deduction-based formal verification of workflow-oriented software models
    Autorzy:
    Klimek, R.
    Powiązania:
    https://bibliotekanauki.pl/articles/330429.pdf
    Data publikacji:
    2014
    Wydawca:
    Uniwersytet Zielonogórski. Oficyna Wydawnicza
    Tematy:
    formal verification
    deductive reasoning
    temporal logic
    semantic tableaux
    workflow pattern
    logical primitive
    generating logical specification
    business model
    BPMN
    formalna weryfikacja
    wnioskowanie dedukcyjne
    logika temporalna
    tablica semantyczna
    wzorzec przepływu pracy
    generowanie specyfikacji logicznej
    model biznesowy
    Opis:
    The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model’s behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is based on the semantic tableaux method, which has some advantages when compared with traditional deduction strategies. The algorithm for automatic generation of logical specifications is proposed. The generation procedure is based on predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of business processes. The main idea behind the approach is to consider patterns, defined in terms of temporal logic, as a kind of (logical) primitives which enable the transformation of models to temporal logic formulas constituting a logical specification. Automation of the generation process is crucial for bridging the gap between the intuitiveness of deductive reasoning and the difficulty of its practical application when logical specifications are built manually. This approach has gone some way towards supporting, hopefully enhancing, our understanding of deduction-based formal verification of workflow-oriented models.
    Źródło:
    International Journal of Applied Mathematics and Computer Science; 2014, 24, 4; 941-956
    1641-876X
    2083-8492
    Pojawia się w:
    International Journal of Applied Mathematics and Computer Science
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Some Puzzles about Molinist Conditionals
    Wybrane problemy molinistycznych okresów warunkowych
    Autorzy:
    Koons, Robert C.
    Powiązania:
    https://bibliotekanauki.pl/articles/2097333.pdf
    Data publikacji:
    2022-03-31
    Wydawca:
    Katolicki Uniwersytet Lubelski Jana Pawła II. Towarzystwo Naukowe KUL
    Tematy:
    molinizm
    okresy warunkowe
    kontrfaktyczne okresy warunkowe wolności
    Boska wolność
    wolność woli
    wiedza pośrednia
    inkompatybilizm
    cyrkularność
    Harry Frankfurt
    Ockham
    logika temporalna
    Molinism
    subjunctive conditionals
    counterfactuals of freedom
    divine freedom
    freedom of the will
    Middle Knowledge
    incompatibilism
    circularity
    temporal logic
    Opis:
    William Hasker has been one of the most trenchant and insightful critics of the revival of Molinism. He has focused on the “freedom problem”, a set of challenges designed to show that Molinism does not secure a place for genuinely free human action (Hasker 1986, 1995, 1999, 2000a, 2000b, 2011). These challenges focus on a key element in the Molinist story: the counterfactual (or subjunctive) conditionals of creaturely freedom. According to Molinism, these conditionals have contingent truth-values that are knowable to God prior to His decision of what world to actualize. This divine “middle knowledge” is supposed to enable God to execute a detailed plan for world history without any loss of creaturely freedom. Hasker has argued that this middle knowledge nonetheless deprives us of the power to do otherwise than we do, a crucial element in human freedom and responsibility. I hope to accomplish three things in this paper. First, I want to step back a bit and explore the nature of the conditionals of creaturely free decision-making (the CCFs), bringing out some of the difficulties in delimiting their scope and nature. Second, I will explore the implications of different answers to an important question that has not been addressed in the literature: whether we have counterfactual power over the conditionals of divine freedom. And, third, I would like to recommend to Molinists a revision that offers a solution to the freedom problem.
    William Hasker był jednym z najbardziej stanowczych i wnikliwych krytyków odrodzenia molinizmu. Skupił się on na „problemie wolności”, czyli na grupie wyzwań, które mają pokazać, że molinizm nie pozostawia miejsca na prawdziwie wolne działanie człowieka (Hasker 1986, 1995, 1999, 2000a, 2000b, 2011). Wyzwania te koncentrują się na kluczowym elemencie narracji tego jezuickiego ruchu: kontrfaktycznych okresach warunkowych wolności stworzeń. Według molinistów, te okresy warunkowe posiadają wartości logiczne, które były znane Bogu przed jego decyzją o tym, który możliwy świat chce urzeczywistnić. Ta Boska „wiedza pośrednia” ma umożliwić Bogu realizację szczegółowego planu dla historii świata bez naruszenia wolności stworzeń. Hasker twierdził jednak, że owa wiedza pośrednia pozbawia nas zdolności do czynienia inaczej (niż czynimy), co jest przecież kluczowym elementem ludzkiej wolności i odpowiedzialności. Autor artykułu stawia sobie trzy cele. Po pierwsze, zamierza zbadać naturę okresów warunkowych wolnych decyzji stworzeń, ukazując niektóre trudności w określeniu ich zakresu i natury. Po drugie, chce rozpatrzyć konsekwencje różnych odpowiedzi na ważne pytanie, które jak dotąd nie zostało poruszone w literaturze przedmiotu: czy posiadamy kontrfaktyczną władzę nad okresami warunkowymi boskiej wolności? I po trzecie, autor chciałby zarekomendować molinistom pewną poprawkę, która pozwoli na rozwiązanie problemu wolności.
    Źródło:
    Roczniki Filozoficzne; 2022, 70, 1; 137-154
    0035-7685
    Pojawia się w:
    Roczniki Filozoficzne
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Modelowanie dynamicznych zjawisk w planowaniu przestrzennym z wykorzystaniem ontologii formalnych
    Modeling of dynamic phenomena in spatial planning with the use of formal ontology
    Autorzy:
    Łukowicz, J.
    Iwaniak, A.
    Strzelecki, M.
    Kaczmarek, I.
    Powiązania:
    https://bibliotekanauki.pl/articles/345837.pdf
    Data publikacji:
    2014
    Wydawca:
    Polskie Towarzystwo Informacji Przestrzennej
    Tematy:
    ontologia
    modelowanie
    planowanie przestrzenne
    Description Logic
    ontologia formalna
    model czasoprzestrzenny
    ontology
    modeling
    spatial planning
    description logic
    formal ontology
    spatio-temporal model
    Opis:
    Zarówno gospodarka przestrzenna jak i planowanie przestrzenne maja charakter multidyscyplinarny oraz odnoszą się do dynamicznie zmieniającej się rzeczywistości. Decyzje projektowe oddziałują na spójność systemu środowiska przyrodniczego. Poprawa jakości zarządzania przestrzenią zależy od wypracowania lepszych metod planowania i przewidywania skutków przekształceń przestrzennych dla środowiska. Takie możliwości dają ontologie oparte na logice opisowej (Description Logic) i związanych z nim systemami wnioskowania. Ontologie mogą być wzbogacane o dodatkowe systemy formalne. Autorzy prezentują sposoby budowania ontologii dziedzinowych dla planowania przestrzennego uzupełnionych przez konstrukcje logiki temporalnej. Jako rezultat, analizy relacji przestrzennych będą rozszerzone o badanie relacji czasowych. Modele czasoprzestrzenne z konstrukcjami logiki temporalnej mogą być przedmiotem wnioskowania wykorzystującego tzw. reasonery (resoning engines). Czasoprzestrzenne reprezentacje są oferowane przez tzw. ontologie wyższego rzędu, w tym przypadku ontologie fundamentalne (formalne). Do tych ontologii można zaliczyć GFO, BFO, DOLCE, OCHRE i inne. Takie ontologie są użyteczne dla modelowania danych przestrzennych z uwzględnieniem ich dynamiki i zmian. Czynią one możliwe przewidywanie scenariuszy przekształceń przestrzennych i przewidywania przyszłego stanu zagospodarowania oraz środowiska.
    Spatial management and spatial planning both have a multidisciplinary nature and refer to dynamically changing reality. Design decisions can affect the integrity of the environmental system. Improvement of spatial management depends on better methods of planning and forecasting about the environmental effects of development change. Such approach is offered by ontologies, based on Description Logics (DL) and related to them inference systems. Ontologies can be enriched with additional logical systems. The authors present a way of building domain ontologies for spatial planning supplemented by structures of temporal logic. As a result, the analysis for exploring the topological relations between spatial objects will be extended to include temporal relationships. Spatiotemporal models with temporal logic structures could be a subject of inference process, performed by reasoner engines. Spatiotemporal representations are offered by so-called upper ontologies in this case group of fundamental ontologies. The set of such ontologies includes GFO, BFO, OCHRE and others. Such ontologies are useful for modeling of spatial data with focus on their dynamics of changes. They make possible a prediction of scenarios of expected spatial transformation and forecasting a future state of spatial development and environmental conditions.
    Źródło:
    Roczniki Geomatyki; 2014, 12, 1(63); 81-91
    1731-5522
    2449-8963
    Pojawia się w:
    Roczniki Geomatyki
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
      Wyświetlanie 1-23 z 23

      Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies