| 1. |
|
|
| 2. |
- Berg, Therese, et al.
(författare)
-
Insights to Angluin's Learning
- 2005
-
Ingår i: Electr. Notes on Theoret. Comput. Sci.. ; 118, s. 3-18
-
Tidskriftsartikel (refereegranskat)
|
|
| 3. |
|
|
| 4. |
- Berg, Therese, et al.
(författare)
-
Insights to Angluin's Learning
- 2005
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 118, s. 3-18
-
Tidskriftsartikel (refereegranskat)abstract
- Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied. A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples. We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results.
|
|
| 5. |
- Berg, Therese, et al.
(författare)
-
Insights to Angluin's Learning
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied. A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples. We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results.
|
|
| 6. |
|
|
| 7. |
- Bollig, Benedikt, et al.
(författare)
-
Deciding LTL over Mazurkiewicz traces
- 2003
-
Ingår i: Data & Knowledge Engineering. - 0169-023X. ; 44:2, s. 221-240
-
Tidskriftsartikel (refereegranskat)
|
|
| 8. |
|
|
| 9. |
|
|
| 10. |
|
|
| 11. |
- Colombo, Christian, et al.
(författare)
-
COST Action IC1402 Runtime Verification Beyond Monitoring
- 2018
-
Ingår i: 18th International Conference on Runtime Verification (RV'18), vol. 11237 of LNCS, pages 18-26. - : Springer.
-
Konferensbidrag (refereegranskat)abstract
- In this paper we report on COST Action IC1402 which studies Runtime Verification approaches beyond Monitoring. COST Actions are funded by the European Union and are an efficient networking instrument for researchers, engineers and scholars to cooperate and coordinate research activities. This COST action IC1402 lasted over the past four years, involved researchers from 27 different European countries and Australia and allowed to have many different working group meetings, workshops and individual visits.
|
|
| 12. |
- Grinchtein, Olga, et al.
(författare)
-
Inference of Timed Transition Systems
- 2005
-
Ingår i: Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY).
-
Konferensbidrag (refereegranskat)
|
|
| 13. |
- Grinchtein, Olga, et al.
(författare)
-
Learning of Event-Recording Automata
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In regular inference, a regular language is inferred from answers to a finite set of membership queries, each of which asks whether the language contains a certain word. One of the most well-known regular inference algorithms is the L* algorithm due to Dana Angluin. However, there are almost no extensions of these algorithms to the setting of timed systems. We extend Angluin's algorithm for on-line learning of regular languages to the setting of timed systems. Since timed automata can freely use an arbitrary number of clocks, we restrict our attention to systems that can be described by deterministic event-recording automata (DERAs). We present three algorithms, TLsg*, TLnsg* and TLs*, for inference of DERAs. In TLsg* and TLnsg*, we further restrict event-recording automata to be event-deterministic in the sense that each state has at most one outgoing transition per action; learning such an automaton becomes significantly more tractable. The algorithm TLnsg* builds on TLsg*, by attempts to construct a smaller (in number of locations) automaton. Finally, TLs* is a learning algorithm for a full class of deterministic event-recording automata, which infers a so called simple DERA, which is similar in spirit to the region graph.
|
|
| 14. |
- Grinchtein, Olga, et al.
(författare)
-
Learning of event-recording automata
- 2004
-
Ingår i: FORMATS/FTRTFT 2004. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 3540231676 ; , s. 379-396
-
Konferensbidrag (refereegranskat)
|
|
| 15. |
- Grinchtein, Olga, et al.
(författare)
-
Learning of event-recording automata
- 2010
-
Ingår i: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 411:47, s. 4029-4054
-
Tidskriftsartikel (refereegranskat)
|
|
| 16. |
- Grinchtein, Olga, et al.
(författare)
-
Network invariants for real-time systems
- 2004
-
Ingår i: 5th International Workshop on Verification of Infinite-State Systems. ; , s. 57-74
-
Konferensbidrag (refereegranskat)
|
|
| 17. |
|
|
| 18. |
- Kharraz, Karam, et al.
(författare)
-
Synchronous Agents, Verification, and Blame - A Deontic View
- 2023
-
Ingår i: Theoretical Aspects of Computing (ICTAC). - : Springer. - 9783031479625
-
Konferensbidrag (refereegranskat)abstract
- A question we can ask of multi-agent systems is whether the agents’ collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, or a specification is violated, a pertinent question is whether any agent is to blame. This paper considers a two-agent synchronous setting and a formal language to specify when agents’ collaboration is required. We take a deontic approach and use obligations, permissions, and prohibitions to capture notions of non-interference between agents. We also handle reparations, allowing violations to be corrected or compensated. We give trace semantics to our logic, and use it to define blame assignment for violations. We give an automaton construction for the logic, which we use as the base for model checking and blame analysis. We also further provide quantitative semantics that is able to compare different interactions in terms of the required reparations.
|
|
| 19. |
- Kharraz, Karam Younes, et al.
(författare)
-
Timed Dyadic Deontic Logic
- 2021
-
Ingår i: Legal Knowledge and Information Systems (JURIX ), vol. 346. Series: Frontiers in Artificial Intelligence and Applications. - : IOS Press. - 0922-6389.
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we introduce TDDL, a timed dyadic deontic logic. Our starting point is a version of a dyadic deontic logic with conditional obligations, permissions, and obligations, and with a ``reparation'' operator for representing contrary-to-duties and contrary-to-prohibitions. We also consider a sequence operator allowing us to define norms as sequences of individual norms and most importantly with timed intervals, allowing us to express deadlines of norms. We provide a trace semantics capturing both satisfaction and violation of norms and discuss fulfilment of TDDL specifications.
|
|
| 20. |
- Leucker, Martin, et al.
(författare)
-
Dynamic Message Sequence Charts
- 2002
-
Ingår i: FSTTCS 2002. - 3540002251 ; , s. 253-264
-
Konferensbidrag (refereegranskat)
|
|
| 21. |
|
|
| 22. |
|
|
| 23. |
|
|
| 24. |
|
|
| 25. |
|
|
| 26. |
- Pretschner, Alexander, et al.
(författare)
-
Model-Based Testing - A Glossary
- 2005
-
Ingår i: Model-Based Testing of Reactive Systems. - : Springer. - 3540262784 ; , s. 607-609
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)
|
|
| 27. |
- Sánchez, César, et al.
(författare)
-
Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions
- 2018
-
Ingår i: ISoLA (4), vol. 11247 of LNCS 2018: 275-279. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- © Springer Nature Switzerland AG 2018. The popularization of blockchain technologies have brought a sudden interest in software that executes on top of blockchain, the so called smart contracts, with many potential applications, from financial contracts to unforgeable elections. Smart contracts are pieces of software that manipulate the shared data stored in the blockchain, with the promise that no central authority can forge or manipulate the execution or its results. This promise also involves an important risk, as well-intentioned users cannot easily roll-back undesired effects due to errors, or prevent other users from finding and exploiting loop-holes in deployed smart contracts. In this ISoLA track we seek to attract a variety of experts in the different aspects of smart contract reliability, discuss the state of the art and explore avenues for future research.
|
|
