BEGIN:VCALENDAR
PRODID:-//davical.org//NONSGML AWL Calendar//EN
VERSION:2.0
CALSCALE:GREGORIAN
X-WR-CALNAME:CFV
BEGIN:VEVENT
CREATED:20121003T153233Z
LAST-MODIFIED:20121029T101539Z
DTSTAMP:20121029T101539Z
UID:e4e9941e-7bea-43ac-b35c-6177512d3318
SUMMARY:[cfv seminar] Nir Piterman (U. Leicester)
DTSTART;TZID=Europe/Paris:20121026T140000
DTEND;TZID=Europe/Paris:20121026T153000
LOCATION:"Rotule" 2NO8.08 (eighth floor)
DESCRIPTION:Title:\n p-Automata and Obligation Games\n\nAbstract:\n
We present our automata-based approach to probabilistic verification.\
nThis new approach adapts notions and techniques from alternating tree\n
automata to the realm of Markov chains.\nThe resulting p-automata determ
ine languages of Markov chains.\nIn order to determine acceptance of Mar
kov chains by p-automata we\ndevelop a new notion of games\, which we ca
ll \\emph{obligation games}.\nIntuitively\, one player commits to achiev
ing a certain probability of\nwinning in the interaction.\n\nWe survey t
he initial results regarding obligation games and p-automata.\nThese inc
lude algorithms for solving obligation parity games\, initial\nresults a
bout the expressive power of p-automata\, and the relation\nbetween p-au
tomata and pCTL model checking.\nIn particular\, these initial foundatio
ns show that p-automata enable\nabstraction-based probabilistic model ch
ecking for probabilistic\nspecifications that subsume Markov chains\, an
d LTL and CTL* like\nlogics.\nMany interesting questions remain open.\nF
or example\, further algorithmic studies of obligation games\,\nthe theo
ry of p-automata\, and the usage in practice of p-automata as an\nabstra
ction framework for Markov chains.\n\nJoint work with:\nKrishnendu Chatt
erjee\, Michael Huth\, and Daniel Wagner
SEQUENCE:3
X-MOZ-GENERATION:6
END:VEVENT
BEGIN:VEVENT
CREATED:20121003T153701Z
LAST-MODIFIED:20121029T101642Z
DTSTAMP:20121029T101642Z
UID:4f079739-edba-462a-90cf-092f9e0f2842
SUMMARY:[cfv seminar] Youssouf Oualhadj (LaBRI)
DTSTART;TZID=Europe/Paris:20121026T160000
DTEND;TZID=Europe/Paris:20121026T170000
LOCATION:"Rotule" 2NO8.08 (eighth floor)
DESCRIPTION:Title:\n Deciding the Value 1 Problem for Probabilistic L
eaktight Automata\n\nAbstract:\n The value 1 problem is a decision pr
oblem for probabilistic automata over finite words: given a probabilisti
c automaton A\, are there words accepted by A with probability arbitrari
ly close to 1?\n\nThis problem was proved undecidable recently. We sharp
en this result\, showing that the undecidability holds even if the proba
bilistic automata have only one probabilistic transition.\n\nOur main co
ntribution is to introduce a new class of probabilistic automata\, calle
d leaktight automata\, for which the value 1 problem is shown decidable
(and PSPACE-complete). We construct an algorithm based on the computatio
n of a monoid abstracting the behaviors of the automaton\, and rely on a
lgebraic techniques developed by Simon for the correctness proof. The cl
ass of leaktight automata is decidable in PSPACE\, subsumes all subclass
es of probabilistic automata whose value 1 problem is known to be decida
ble (in particular deterministic automata)\, and is closed under two nat
ural composition operators.\n
TRANSP:OPAQUE
X-MOZ-GENERATION:3
SEQUENCE:2
END:VEVENT
BEGIN:VEVENT
CREATED:20121029T101708Z
LAST-MODIFIED:20121105T093507Z
DTSTAMP:20121105T093507Z
UID:539763b1-5947-4125-ba20-55c0c5679678
SUMMARY:[cfv seminar] Erich Grädel (RTWH Aachen)
DTSTART;TZID=Europe/Paris:20121214T140000
DTEND;TZID=Europe/Paris:20121214T153000
LOCATION:NO Solvay (5th floor)
TRANSP:OPAQUE
DESCRIPTION:Title:\n Banach-Mazur Games on Graphs\n\n\nAbstract:\n\nInf
nite games where two players take turns to move a token through a direct
ed graph\, thus tracing out an infinite path\, have numerous application
s in different branches of mathematics and computer science. In the clas
sical format of such games\, the possible moves of the players are given
by the edges of the graph\; in each move a player takes the token from
its current position along an edge to a next position. In Banach-Mazur g
ames the players instead select in each move a path of arbitrary finite
length rather than just an edge. In both cases the outcome of a play is
an infinite path and the objectives of the players are given by properti
es of infinite paths.\n\nBanach-Mazur games have a long tradition in des
criptive set theory and topology\, and have recently been shown to have
also interesting applications in computer science\, such as for planning
in nondeterministic domains\, the study of fairness in concurrent syste
ms and for timed automata.\n\nWe discuss several notions of ”simple” win
ning strategies for Banach-Mazur games on graphs\, such as positional st
rategies\, move-counting or length-counting strategies\, and strategies
with a memory based on finite appearance records (FAR). Banach-Mazur gam
es often admit stronger determinacy results than classical graph games a
nd more efficient algorithmic solutions. For instance\, all Banach-Mazur
games with omega-regular winning conditions are positionally determined
. Beyond the omega-regular winning conditions\, we focus here on Muller
conditions with infinitely many colours. We investigate the infinitary M
uller conditions that guarantee positional determinacy for Banach-Mazur
games. Further\, we determine classes of such conditions that require in
finite memory but guarantee determinacy via move-counting strategies\, l
ength-counting strategies\, and FAR-strategies. We also discuss the rela
tionships between these different notions of determinacy.
X-MOZ-GENERATION:1
END:VEVENT
BEGIN:VEVENT
CREATED:20180430T073728Z
UID:28E7BECD-BCD0-4EAB-8E45-1412260A34C2
DTEND;TZID=Europe/Brussels:20180511T121500
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Shibashis Guha (ULB)
DTSTART;TZID=Europe/Brussels:20180511T114500
DTSTAMP:20180430T073818Z
LOCATION:ULB campus La Plaine\, Building NO\, Salle Solvay
SEQUENCE:0
END:VEVENT
BEGIN:VEVENT
CREATED:20121126T185025Z
LAST-MODIFIED:20121126T185306Z
DTSTAMP:20121126T185306Z
UID:24ec4c8d-63d1-6b4a-b882-99e2a00bace5
SUMMARY:[cfv seminar] Thomas Brihaye (U. Mons)
DTSTART;TZID=Europe/Paris:20121130T160000
DTEND;TZID=Europe/Paris:20121130T170000
LOCATION:NO Solvay (5th floor)
DESCRIPTION:Title:\n Multiplayer cost games with simple Nash equilibr
ia\n\nAbstract:\n Multiplayer games with selfish agents naturally occ
ur in the design of distributed and embedded-systems. As the goals of se
lfish agents are usually neither equivalent nor antagonistic to each oth
er\, such games are non zero-sum games. We study such games and show tha
t a large class of these games\, including games where the individual ob
jectives are mean- or discounted-payoff\, or quantitative reachability\,
and show that they do not only have a solution\, but a simple solution.
We establish the existence of Nash equilibria that are composed of k me
moryless strategies for each agent in a setting with k agents\, one main
and k-1 minor strategies. The main strategy describes what happens when
all agents comply\, whereas the minor strategies ensure that all other
agents immediately start to co-operate against the agent who first devia
tes from the plan. This simplicity is important\, as rational agents are
an idealisation. Realistically\, agents have to decide on their moves w
ith very limited resources\, and complicated strategies that require exp
onential — or even non-elementary — implementations cannot realistically
be implemented. The existence of simple strategies that we prove in thi
s paper therefore holds a promise of implementability.\n\n This is a
joint work with Julie De Pril and Sven Schewe.\n
END:VEVENT
BEGIN:VEVENT
CREATED:20121029T101442Z
LAST-MODIFIED:20121126T185338Z
DTSTAMP:20121126T185338Z
UID:019950af-c80b-41e7-b85f-15f5aca5dc50
SUMMARY:[cfv seminar] Roland Meyer (U. Kaiserslautern)
DTSTART;TZID=Europe/Paris:20121130T140000
DTEND;TZID=Europe/Paris:20121130T153000
LOCATION:NO Solvay (5th floor)
TRANSP:OPAQUE
DESCRIPTION:Title:\n Verification of Concurrent Programs under Relaxe
d Memory Models \n\nAbstract:\n Programmers often assume concurrent p
rograms run on sequentially consistent (SC) processors that interleave t
he actions in different threads but execute the actions of each thread i
n program order. This assumption\, however\, does not hold for modern pr
ocessors. For performance reasons\, recent hardware only implements rela
xed memory models where actions may be executed out-of-program-order. Pr
ograms that run on relaxed memories may show undesirable behavior that i
s impossible under SC. With the trend towards multicore machines\, bugs
due to relaxed memory models become a serious problem in mainstream prog
ramming that calls for a solution.\n\n This talk provides an overview
of recent results on the verification of concurrent programs that run o
n relaxed memory models. We concentrate on the Total Store Ordering mode
l that is implemented in x86 processors\, and discuss the reachability a
nd the robustness problems. Given a concurrent program and a configurati
on\, reachability checks whether the program admits a run that leads to
this configuration. Robustness checks whether the behavior of a given pr
ogram on a relaxed memory model coincides with the expected SC semantics
. Both problems have been shown to be decidable\, but with very differen
t complexity.
X-MOZ-GENERATION:1
END:VEVENT
BEGIN:VEVENT
CREATED:20121126T185356Z
LAST-MODIFIED:20121126T185603Z
DTSTAMP:20121126T185603Z
UID:678b2ee3-d96c-bb49-b2f1-f62eb346c92d
SUMMARY:[cfv seminar] Jean-François Raskin (ULB)
DTSTART;TZID=Europe/Paris:20121214T160000
DTEND;TZID=Europe/Paris:20121214T170000
LOCATION:NO Solvay (5th floor)
DESCRIPTION:Title:\n Multi-dimension Quantitative Games: Complexity a
nd Strategy Synthesis\n\nAbstract:\n In mean-payoff games\, the objec
tive of the protagonist is to ensure that the limit average of an infini
te sequence of numeric weights is nonnegative. In energy games\, the obj
ective is to ensure that the running sum of weights is always nonnegativ
e. Multi-mean-payoff and multi-energy games replace individual weights b
y tuples\, and the limit average (resp. running sum) of each coordinate
must be (resp. remain) nonnegative. These games have applications in the
synthesis of resource-bounded processes with multiple resources. In thi
s talk\, I will summarize several recent results that we have obtained r
ecently:\n - We prove the finite-memory determinacy of multi-energy g
ames and show the inter-reducibility of multi-mean-payoff and multi-ener
gy games for finite-memory strategies.\n - We improve the computation
al complexity for solving both classes of games with finite-memory strat
egies: while the previously best known upper bound was ExpSpace\, and no
lower bound was known\, we give an optimal coNP-complete bound. For mem
oryless strategies\, we show that the problem of deciding the existence
of a winning strategy for the protagonist is NP-complete.\n - We prov
ide an optimal symbolic and incremental algorithm to synthesis strategie
s in multi-energy games.\n - We present the first solution of multi-m
ean-payoff games with infinite-memory strategies. We show that multi-mea
n-payoff games with mean-payoff-sup objectives can be decided in NP and
in coNP\, whereas multi-mean-payoff games with mean-payoff-inf objective
s are coNP-complete.\n\n
END:VEVENT
BEGIN:VEVENT
CREATED:20180430T073821Z
UID:72D57A6B-0D77-41A7-87B0-C238B5F2F419
DTEND;TZID=Europe/Brussels:20180511T163000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Nicolas Mazzocchi (ULB)
DTSTART;TZID=Europe/Brussels:20180511T160000
DTSTAMP:20180430T073858Z
LOCATION:ULB la Plaine\, Building NO\, Salle Solvay
SEQUENCE:0
END:VEVENT
BEGIN:VEVENT
CREATED:20121015T113806Z
LAST-MODIFIED:20130110T150318Z
DTSTAMP:20130110T150318Z
UID:62672e99-ff99-4fc0-9c2a-02ae595eecf0
SUMMARY:[cfv seminar] Aniello Murano (Università degli Studi di Napoli F
ederico II)
DTSTART;TZID=Europe/Paris:20130125T140000
DTEND;TZID=Europe/Paris:20130125T153000
DESCRIPTION:Title: \n Pushdown Module Checking with Perfect and Imperfe
ct Information\n\nAbstract:\n Model checking is a useful method to veri
fy automatically the correctness of a system with respect to a desired b
ehavior by checking whether a mathematical model of the system satisfies
a formal specification of this behavior. Many systems of interest are o
pen\, in the sense that their behavior depends on the interaction with t
heir environment. The model checking problem for finite-state open syste
ms (called module checking) has been intensively studied in the literatu
re.\n\n In this talk\, we first recall the basic concepts and the main
results regarding module checking.\nThen\, we focus on open pushdown sys
tems and consider the related model-checking problem (pushdown module ch
ecking\, for short) with respect to properties expressed by CTL\, CTL*\,
and µ-calculus formulas\, both in the perfect and imperfect information
settings.\n\n First we show that\, in the perfect information setting\
, pushdown module checking against CTL and µ-calculus formulas is 2Expti
me-complete\, while it is 3Exptime-complete with respect to CTL* formula
s. In particular\, we show that\, for a fixed formula\, the problem is E
xptime-complete.\n\n Then\, we consider the previous problems in the im
perfect information setting\, i.e.\, in the case where the environment h
as only a partial view of system's control states and pushdown store con
tent.\nWe show that pushdown module checking becomes undecidable when th
e environment has imperfect information about the pushdown store\, while
having only imperfect information about the control states\,\nbut a vis
ible pushdown store\, makes the problem decidable and 2Exptime-complete
for CTL and the propositional µ-calculus formulas\, and 3Exptime-complet
e in the case of CTL* formulas.\n\n We conclude the talk by considering
restricted open pushdown models in which it is possible\, for fixed for
mulas\, to solve the pushdown module checking problem in polynomial time
.
LOCATION:NO Solvay (5th floor)
TRANSP:OPAQUE
SEQUENCE:1
X-MOZ-GENERATION:5
END:VEVENT
BEGIN:VEVENT
CREATED:20121204T102655Z
LAST-MODIFIED:20130106T221426Z
DTSTAMP:20130106T221426Z
UID:cf864230-1fc9-4457-b896-89fee6866a39
SUMMARY:[cfv seminar] Pavithra Prabhakar (IMDEA Software Institute)
DTSTART;TZID=Europe/Paris:20130222T140000
DTEND;TZID=Europe/Paris:20130222T153000
LOCATION:NO Solvay (5th floor)
DESCRIPTION:Title:\n Scalable Verification of Hybrid Systems\n\nAbstr
act:\n The increasing demand for automation in safety-critical applic
ations such as aeronautics\, automotive\, industrial process control\, m
edical devices and so on\, has pressurized the need for scalable formal
analysis techniques for ensuring reliable and error-free operation of th
e systems. A unique feature of these systems is the mixed discrete conti
nuous behaviors they exhibit\, which is due to the interaction between a
digital computer controlling a physical entity. From the point of view
of computability\, presence of the continuous dynamics makes the problem
challenging so much so that the verification of even simple properties
becomes un-decidable for a class of systems with fairly simple continuou
s dynamics. Approximations have proven to be a key component in dealing
with the state space explosion resulting from the hybrid models. In this
talk\, I will discuss various approximation techniques for different cl
asses of systems and properties\, including\, counter-example guided abs
traction refinement and bounded error-approximations.
TRANSP:OPAQUE
X-MOZ-GENERATION:1
END:VEVENT
BEGIN:VEVENT
CREATED:20130110T100128Z
LAST-MODIFIED:20130215T103959Z
DTSTAMP:20130215T103959Z
UID:f53bb7a5-93d1-4c08-a7a0-0729f3bc74b2
SUMMARY:[cfv seminar] Mickaël Randour (UMONS)
DTSTART;TZID=Europe/Paris:20130329T160000
DTEND;TZID=Europe/Paris:20130329T170000
TRANSP:OPAQUE
X-MOZ-GENERATION:2
LOCATION:NO Solvay (5th floor)
SEQUENCE:1
DESCRIPTION:Title:\n Looking at Mean-Payoff and Total-Payoff through
Windows\n\nAbstract:\n We consider two-player games played on weighte
d directed graphs with mean-payoff and total-payoff objectives\, which a
re two classical quantitative objectives. While for single-dimensional o
bjectives all results for mean-payoff and total-payoff coincide\, we sho
w that in contrast to multi-dimensional mean-payoff games that are known
to be coNP-complete\, multi-dimensional total-payoff games are undecida
ble. We introduce conservative approximations of these objectives\, wher
e the payoff is considered over a local finite window sliding along a pl
ay\, instead of the whole play. For single dimension\, we show that (i)
if the window size is polynomial\, then the problem can be solved in pol
ynomial time\, and (ii) the existence of a bounded window can be decided
in NP ∩ coNP\, and is at least as hard as solving mean-payoff games. Fo
r multiple dimensions\, we show that (i) the problem with fixed window s
ize is EXPTIME-complete\, and (ii) there is no primitive-recursive algor
ithm to decide the existence of a bounded window.\n
END:VEVENT
BEGIN:VEVENT
CREATED:20121015T113806Z
LAST-MODIFIED:20130116T150432Z
DTSTAMP:20130116T150432Z
UID:65e21a78-d779-4055-bae6-0561abfe9d9b
SUMMARY:[cfv seminar] Romain Brenguier (ULB)
DTSTART;TZID=Europe/Paris:20130125T160000
DTEND;TZID=Europe/Paris:20130125T170000
DESCRIPTION:Title: \n Nash Equilibria in Concurrent and Timed Games\n\n
Abstract:\n We study multi-player concurrent and timed games. These two
classes of games have been useful models in controller synthesis. In si
tuations where several agents interact\, the notion of winning strategie
s used in the past is not adapted and it is necessary to adopt solution
concepts from game theory. The main concept considered in this area is t
hat of Nash equilibrium.\n\n For concurrent games\, we propose a transf
ormation which draw a parallel between equilibria and winning strategies
. Many works have focused on the computation of winning strategies and w
e can take advantage of the available algorithms. To compute equilibria
in timed games we show that it is possible to reduce them to concurrent
games.
LOCATION:NO Solvay (5th floor)
TRANSP:OPAQUE
SEQUENCE:1
X-MOZ-GENERATION:6
END:VEVENT
BEGIN:VEVENT
CREATED:20121204T102655Z
LAST-MODIFIED:20130131T092313Z
DTSTAMP:20130131T092313Z
UID:0368454b-3768-461b-acdb-6b757a54bc53
SUMMARY:[cfv seminar] Alexander Linden (ULg)
DTSTART;TZID=Europe/Paris:20130222T160000
DTEND;TZID=Europe/Paris:20130222T170000
LOCATION:NO Solvay (5th floor)
TRANSP:OPAQUE
X-MOZ-GENERATION:3
DESCRIPTION:Title:\n A Verification-Based Approach to Memory Fence In
sertion in PSO Memory Systems\n\nAbstract:\n This talk addresses the
problem of verifying and correcting programs when they are moved from a
sequential consistency execution environment to a relaxed memory context
. Specifically\, it considers the PSO (Partial Store Order) memory model
\, which corresponds to the use of a store buffer for each shared variab
le and each process. We also will consider\, as an intermediate step\, t
he TSO (Total Store Order) memory model\, which corresponds to the use o
f one store buffer per process.\n\n The proposed approach extends a p
reviously developed verification tool that uses finite automata to symbo
lically represent the possible contents of the store buffers. Its starti
ng point is a program that is correct for the usual Sequential Consisten
cy (SC) memory model\, but that might be incorrect under PSO with respec
t to safety properties. This program is then first analyzed and correcte
d for the TSO memory model\, and then this TSO-safe program is analyzed
and corrected under PSO\, producing a PSO-safe program. To obtain a TSO-
safe program\, only store-load fences (TSO only allows store-load relaxa
tions) are introduced into the program. Finaly\, to produce a PSO-safe p
rogram\, only store-store fences (PSO additionally allows store-store re
laxations) are introduced.\n\n An advantage of our technique is that
the underlying symbolic verification tool makes a full exploration of pr
ogram behaviors possible even for cyclic programs\, which makes our appr
oach broadly applicable. The method has been tested with an experimental
implementation and can effectively handle a series of classical example
s.
END:VEVENT
BEGIN:VEVENT
CREATED:20130129T144135Z
LAST-MODIFIED:20130204T144003Z
DTSTAMP:20130204T144003Z
UID:2f595961-7ffe-4c07-8df4-43b764f83d74
SUMMARY:[cfv] Francqui chair: Wolfgang Thomas
ATTACH;FMTTYPE=;ENCODING=:http://informatique.umons.ac.be/tcs/Francqui/
DTSTART;TZID=Europe/Paris:20130418T170000
DTEND;TZID=Europe/Paris:20130418T200000
DESCRIPTION:[17:00-17:30] Welcome\n[17:30-19:00] Logic\, Algorithms\, an
d Automata: A Historical Journey\n[19:00] Reception\n\nAttendance is fre
e\, but registration is required
LOCATION:Centre Vésale\, Campus de la Plaine de Nimy\, Université de Mon
s\, Mons (Belgium)
X-MOZ-GENERATION:3
TRANSP:OPAQUE
SEQUENCE:1
END:VEVENT
BEGIN:VEVENT
CREATED:20130129T144336Z
LAST-MODIFIED:20130204T144046Z
DTSTAMP:20130204T144046Z
UID:6c757798-a05e-4cfd-b32d-7c411c2226eb
SUMMARY:[cfv] Francqui chair: Wolfgang Thomas
ATTACH:http://informatique.umons.ac.be/tcs/Francqui/
DTSTART;TZID=Europe/Paris:20130426T100000
DTEND;TZID=Europe/Paris:20130426T163000
DESCRIPTION:[10:00-11:00] Results of the Golden 1960’s Revisited\n[11:00
-11:30] Coffee Break\n[11:30-12:30] Prefix Rewriting and the Pushdown Hi
erarchy\n[12:30-14:00] Lunch\n[14:00-15:00] The Composition Method\n[15:
00-15:30] Coffee Break\n[15:30-16:30] Undecidability Results\n\nAttendan
ce is free\, but registration is required
LOCATION:Centre Vésale\, Campus de la Plaine de Nimy\, Université de Mon
s\, Mons (Belgium)
X-MOZ-GENERATION:2
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
CREATED:20130129T144336Z
LAST-MODIFIED:20130204T144107Z
DTSTAMP:20130204T144107Z
UID:4d7035fc-88ee-46dd-ad87-5de0cd9702bd
SUMMARY:[cfv] Francqui chair: Wolfgang Thomas
ATTACH:http://informatique.umons.ac.be/tcs/Francqui/
DTSTART;TZID=Europe/Paris:20130503T100000
DTEND;TZID=Europe/Paris:20130503T163000
DESCRIPTION:[10:00-11:00] The Fundamental Results on Infinite Two-Person
Games\n[11:00-11:30] Coffee Break\n[11:30-12:30] Strategies in a Logica
l Setting\n[12:30-14:00] Lunch\n[14:00-15:00] Concepts of Strategy\n[15:
00-15:30] Coffee Break\n[15:30-16:30] Winning Infinite Games in Finite T
ime\n\nAttendance is free\, but registration is required
LOCATION:Centre Vésale\, Campus de la Plaine de Nimy\, Université de Mon
s\, Mons (Belgium)
X-MOZ-GENERATION:2
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
CREATED:20130110T100128Z
LAST-MODIFIED:20130305T154333Z
DTSTAMP:20130305T154333Z
UID:47500a8e-9784-47af-89d9-f8799d415ed3
SUMMARY:[cfv seminar] Giuseppe Lipari (ENS Cachan)
DTSTART;TZID=Europe/Paris:20130329T140000
DTEND;TZID=Europe/Paris:20130329T153000
TRANSP:OPAQUE
X-MOZ-GENERATION:3
LOCATION:NO Solvay (5th floor)
SEQUENCE:1
DESCRIPTION:Title:\n Component-based analysis of real-time systems\n\
nAbstract:\n\n The complexity of modern embedded real-time systems is
constantly increasing\, as new and more complex functionality is added
to existing software. At the same time\, due to the increasing computati
onal power of the hardware platforms and to the pressure to reduce the c
osts\, software that in the past was run on different computational node
s\, is now being integrated onto a single node.\n\n An appealing way
to reduce complexity is to apply a component-based real-time design meth
odology. A real-time system can be seen as a set of interacting componen
ts\, each one providing a well-defined subset of functionalities\, whose
integration produces the final system behavior. A component-based metho
dology is successful only if it can effectively reduce the complexity. T
o achieve this goal\, the system designer must be able to 1) analyze and
validate each component in isolation from the rest of the system\, 2) s
ummarize its properties and requirements into simpler interfaces\, 3) pe
rform the final integration analysis and validation on the component int
erfaces.\n\n In this talk\, the author will give an overview of curre
nt techniques for component-based analysis of real-time systems\, with a
look at their possible use in avionics and automotive systems. Then\, a
possible research agenda will be discussed\, highlighting the shortcomi
ngs of current analysis and how to improve on it.
END:VEVENT
BEGIN:VEVENT
CREATED:20130828T222738Z
UID:53BC493A-5C8F-4E35-9989-15B3C096E6E7
DTEND;TZID=Europe/Brussels:20131028T180000
TRANSP:OPAQUE
SUMMARY:[cfv] Nord pas de Calais/Belgium Congress of Mathematics @ Valen
ciennes
DTSTART;TZID=Europe/Brussels:20131028T140000
DTSTAMP:20130828T223818Z
SEQUENCE:8
DESCRIPTION:Nicolas Markey\, Quentin Menet\, Mickael Randour\, James Wor
rell\nMonday\, 28 October\, 2013 - 14:00\nValenciennes\, ISTV2 Building\
nMathematics\, game theory\, and verification of complex computer system
s\nOrganizer: T. Brihaye (UMONS)\n\nNicolas Markey (ENS Cachan) — Quanti
fied CTL.\nQuentin Menet (UMONS) — Banach-Mazur games.\nMickael Randour
(UMONS) — Beyond Worst-Case Synthesis in Two-Player Quantitative Games.\
nJames Worrell (Université d'Oxford) — Positivity Problems for Linear Re
currence Sequences.\nAdditional information: https://math.umons.ac.be/np
cbe13/\nRegistration required.
BEGIN:VALARM
X-WR-ALARMUID:56869886-E001-491D-9D32-A5292204A056
UID:56869886-E001-491D-9D32-A5292204A056
TRIGGER;VALUE=DATE-TIME:19760401T005545Z
X-APPLE-DEFAULT-ALARM:TRUE
ACTION:NONE
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20140104T114653Z
UID:F499B6FB-DB48-4D20-AE35-1A5892671C12
DTEND;TZID=Europe/Brussels:20140131T153000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Daniel Le Berre (Université d'Artois)
DTSTART;TZID=Europe/Brussels:20140131T140000
DTSTAMP:20140106T085801Z
LOCATION:Forum C
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=Forum C:
SEQUENCE:9
DESCRIPTION:Title: Solvers and tools to tackle problems in propositional
logic\n\nAbstract: Thanks to the emergence of very efficient SAT engine
s\, the last decade has seen the design of new solvers to tackle other
problems in propositional logic. It is now possible to solve boolean op
timization problems using either Pseudo-Boolean or MAXSAT solvers. Compu
ting a Minimal Unsatisfiable Subformula (or UNSAT core) is now a routine
in several solvers. The aim of this talk is to summarize which kind of
propositional problems can now be solved in practice. We will especially
focus on problems for which the research community provides a common in
put format and multiple solvers. The last part of the talk will present
a tool which allow to model a problem in a friendly domain specific lang
uage and to solve it using a SAT solver.
END:VEVENT
BEGIN:VEVENT
CREATED:20131113T103912Z
UID:0E42EF7F-F681-48F1-A63A-0BCC43D2F10E
DTEND;TZID=Europe/Brussels:20131129T153000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Marta Kwiatkowska (University of Oxford)
DTSTART;TZID=Europe/Brussels:20131129T140000
DTSTAMP:20131122T130015Z
LOCATION:NO Solvay (5th floor)
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=NO Solvay (5th floor):
SEQUENCE:10
DESCRIPTION:Title:\nAutomated Verification and Strategy Synthesis for Pr
obabilistic Systems\n\nAbstract:\nProbabilistic model checking is an aut
omated technique to verify whether\na probabilistic system\, e.g. a dist
ributed network protocol which can\nexhibit failures\, satisfies a tempo
ral logic property\, for example\, the\nminimum probability of the netwo
rk recovering from a fault in a given\ntime period is above 0.98. One ca
n also generate\, given a model and a\ntemporal property\, a strategy fo
r controlling the system in order to\nachieve or optimise the property\,
but this aspect has received less\nattention to date. In this paper\, w
e give an overview of methods for\nautomated verification and strategy s
ynthesis\, focusing on Markov\ndecision process models and temporal logi
cs PCTL and LTL. We also\ndescribe how to apply multi-objective model ch
ecking to investigate\ntrade-offs between the properties. We illustrate
these techniques by\nmeans of several case studies analysed in the PRISM
model checker (www.prismmodelchecker.org). The lecture concludes with a
summary of future challenges in this area.
BEGIN:VALARM
X-WR-ALARMUID:4A03A5AA-5A91-41E4-A421-8A9B668906A6
UID:4A03A5AA-5A91-41E4-A421-8A9B668906A6
TRIGGER;VALUE=DATE-TIME:19760401T005545Z
ACKNOWLEDGED:20131122T130015Z
ACTION:NONE
END:VALARM
BEGIN:VALARM
X-WR-ALARMUID:E9E9366E-1346-4825-8243-8729D0B0E74F
UID:E9E9366E-1346-4825-8243-8729D0B0E74F
TRIGGER:-P1W
ACKNOWLEDGED:20131122T130015Z
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20131114T095429Z
UID:1B7F52B0-7C36-441D-B812-A4B791FBFBD1
DTEND;TZID=Europe/Brussels:20131129T163000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Simon Busard (UC Louvain)
DTSTART;TZID=Europe/Brussels:20131129T160000
DTSTAMP:20131122T150004Z
LOCATION:NO Solvay (5th floor)
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=NO Solvay (5th floor):
SEQUENCE:11
DESCRIPTION:Title: \nReasoning about strategies under partial observabil
ity and fairness constraints\n\nAbstract:Alternating-time Temporal Logic
(ATL) is a logic to reason about strategies that a set of agents can ad
opt to achieve a specified collective goal. ATL can also be used to spec
ify what agents can do in open systems\, where they can interact with th
eir environment in many different ways.\nA number of extensions for this
logic exist\; some of them mix strategies and partial observability\, s
ome others include fairness constraints\, but no work provides a unified
framework for strategies\, partial observability and fairness constrain
ts. Integration of these three concepts is of particular importance when
reasoning about the capabilities of agents that do not have full knowle
dge of a system\, for instance when the agents can assume that the envir
onment behaves in a fair way.\nIn this talk we present ATLK_irF \, a log
ic combining strategies under partial observability and epistemic proper
ties of agents in a system with fairness constraints on states. We intro
duce a model-checking algorithm for ATLK_irF by extending the algorithm
for a full-observability variant of the logic.
BEGIN:VALARM
X-WR-ALARMUID:5527EBD9-A7E2-42B8-8E3D-00B33F66E4B2
UID:5527EBD9-A7E2-42B8-8E3D-00B33F66E4B2
TRIGGER;VALUE=DATE-TIME:19760401T005545Z
ACKNOWLEDGED:20131122T150004Z
ACTION:NONE
END:VALARM
BEGIN:VALARM
X-WR-ALARMUID:FDD30E31-302A-4688-9388-35B6375D37A6
UID:FDD30E31-302A-4688-9388-35B6375D37A6
TRIGGER:-P1W
ACKNOWLEDGED:20131122T150004Z
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20140602T081813Z
UID:58FDF2B6-BC8E-4F84-9769-8545CF99D961
DTEND;TZID=Europe/Brussels:20140606T163000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Julie de Pril (UMONS)
DTSTART;TZID=Europe/Brussels:20140606T160000
DTSTAMP:20140602T081937Z
LOCATION:Room 2NO9.06
SEQUENCE:8
DESCRIPTION:Title: Existence of Secure Equilibrium in Multi-Player Games
with Perfect Information\n\nAbstract: Secure equilibrium is a refinemen
t of Nash equilibrium\, which provides\nsome security to the players aga
inst deviations when a player changes\nhis strategy to another best resp
onse strategy. The concept of secure\nequilibrium is specifically develo
ped for assume-guarantee synthesis\nand has already been applied in this
context. Yet\, not much is known\nabout its existence in games with mor
e than two players. In this\npaper\, we establish the existence of secur
e equilibrium in two classes\nof multi-player perfect information turn-b
ased games: (1) in games\nwith possibly probabilistic transitions\, havi
ng countable state and\nfinite action spaces and bounded and continuous
payoff functions\, and\n(2) in games with only deterministic transitions
\, having arbitrary\nstate and action spaces and Borel payoff functions
with a finite range\n(in particular\, qualitative Borel payoff functions
). We show that\nthese results apply to several types of games studied i
n the\nliterature.
END:VEVENT
BEGIN:VEVENT
CREATED:20131210T175348Z
UID:18792C92-F347-46B0-81D9-4C3EFF3C783E
DTEND;TZID=Europe/Brussels:20140221T153000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Frédéric Mallet (Université Nice Sophia Antipolis)
DTSTART;TZID=Europe/Brussels:20140221T140000
DTSTAMP:20140106T114018Z
LOCATION:Forum E
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=Forum E:
SEQUENCE:8
DESCRIPTION:Title: A tour of MARTE/CCSL: usage\, simulation and verifica
tion\n\nAbstract: In the development of safety-critical embedded systems
\, the ability to\nformally analyze system behavior models\, based on ti
ming and causality\, helps\nthe designer to get insight into the systems
overall timing behavior. To support the\ndesign and analysis of real-ti
me embedded systems\, the UML modeling profile\nfor MARTE provides CCSL
– a time model and a clock constraint specification language.\nCCSL is a
n expressive language that supports specification of both logical\nand c
hronometric constraints for MARTE models. On the other hand\, semantic\n
frameworks such as timed automata provide verification support for real-
time systems.\nTo address the challenge of verifying CCSL-based behavior
models\, we have proposed a\ntechnique for transforming MARTE/CCSL mode
behaviors\ninto Timed Automata for model-checking using the UPPAAL tool
. This enables\nverification of both logical and chronometric properties
of the system\, which has\nnot been possible before.
BEGIN:VALARM
X-WR-ALARMUID:88229F8F-13EB-40BE-93DC-F08F091F050F
UID:88229F8F-13EB-40BE-93DC-F08F091F050F
TRIGGER;VALUE=DATE-TIME:19760401T005545Z
ACTION:NONE
END:VALARM
BEGIN:VALARM
X-WR-ALARMUID:FEEEDDEC-8C3E-40E1-AA10-C6E06B61A6C1
UID:FEEEDDEC-8C3E-40E1-AA10-C6E06B61A6C1
TRIGGER:-P6DT15H
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20131210T175525Z
UID:D2F5B21B-AB8D-4573-AC91-7751AF1EB526
DTEND;TZID=Europe/Brussels:20140221T163000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Eun-Young Kang (Université de Namur)
DTSTART;TZID=Europe/Brussels:20140221T160000
DTSTAMP:20140110T151136Z
LOCATION:Forum E
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=Forum E:
SEQUENCE:10
DESCRIPTION:Title: Enabling Schedulability Analisys for Automotive Syste
ms\n\nAbstract: Modeling and analysis of precise non-functional\npropert
ies\, such as energy and timing constraints\, is key to the\ncorrect dev
elopment of automotive systems. Automotive applications\ndevelopment cos
t\, in particular\, is impacted by incorrect design\nmade at the early d
evelopment phases but only detected later\, often\nafter implementation.
This late detection of design errors leads to\nadditional cost. In the
talk\, we propose a model driven approach to\nperform non-functional pro
perties verification and to enable\nscheduling analysis of automotive sy
stems at the very early design\nlevel. The different phases of a design
range from the requirements\nto a model allocated on a specific executio
n platform: EAST-ADL and\nMARTE are used together to specify the structu
re and energy/timing\nconstraints of the software\, as well as the hardw
are parts of the\nsystem. To prove the correctness of specification and
perform the\nscheduling analysis\, the semantics of the constraints is g
iven as\nmapping to a formal interchange format XFG (eXtended Function-b
lock\nGraphs) language. The XFG models are then automatically translated
\ninto priced timed automata for model checking. This later\ntransformat
ion is supported by a tool chain called A-BeTA (EAST-ADL\nBehavioral Mod
eling and Translation into Analyzable Model). The\napplicability of this
approach is demonstrated on the Brake-By-Wire\ncase study.
BEGIN:VALARM
X-WR-ALARMUID:D5242075-CCA3-4924-A8A7-AC53A0EA329B
UID:D5242075-CCA3-4924-A8A7-AC53A0EA329B
TRIGGER;VALUE=DATE-TIME:19760401T005545Z
ACTION:NONE
END:VALARM
BEGIN:VALARM
X-WR-ALARMUID:DFBB5F79-575E-4954-B4C7-71392DB453FE
UID:DFBB5F79-575E-4954-B4C7-71392DB453FE
TRIGGER:-P6DT15H
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20180109T142451Z
UID:579DBCB5-0188-4403-B0C9-F99524EA31CD
DTEND;TZID=Europe/Brussels:20180427T153000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Pierre Ganty (IMDEA)
DTSTART;TZID=Europe/Brussels:20180427T140000
DTSTAMP:20180117T115637Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
END:VEVENT
BEGIN:VEVENT
CREATED:20140108T103337Z
UID:13047784-60EA-4C1A-8CD5-D6E710AB3A3F
DTEND;TZID=Europe/Brussels:20140131T170000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Nathalie Bertrand (INRIA Rennes)
DTSTART;TZID=Europe/Brussels:20140131T160000
DTSTAMP:20140108T103943Z
LOCATION:Forum C
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=Forum C:
SEQUENCE:6
DESCRIPTION:Title: Active diagnosis for probabilistic systems\n\nAbstrac
t: The diagnosis problem amounts to deciding whether some specific fault
event occurred or not in a system\, given the observations collected on
a run of this system. This system is then diagnosable if the fault can
always be detected\, and the active diagnosis problem consists in contro
lling the system in order to ensure its diagnosability. We consider here
a stochastic framework for this problem: once a control is selected\, t
he system becomes a stochastic process. In this setting\, the active dia
gnosis problem consists in deciding whether there exists some observatio
n-based strategy that makes the system diagnosable with probability one.
We prove that this problem is EXPTIME-complete\, and that the active di
agnosis strategies are belief-based. The safe active diagnosis problem i
s similar\, but aims at enforcing diagnosability while preserving a posi
tive probability to non faulty runs\, i.e. without enforcing the occurre
nce of a fault. We prove that this problem requires non belief-based str
ategies\, and that it is undecidable. However\, it belongs to NEXPTIME w
hen restricted to belief-based strategies. Our work also refines the dec
idability/undecidability frontier for verification problems on partially
observed Markov decision processes.\nThis is a joint work with Éric Fab
re\, Stefan Haar\, Serge Haddad and Loïc Hélouët.
END:VEVENT
BEGIN:VEVENT
CREATED:20140304T043557Z
UID:4AC00661-CC4A-44B9-AEBE-D50C1A4DC0FD
DTEND;TZID=Europe/Brussels:20140328T153000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Jérôme Leroux (CNRS-LaBRI)
DTSTART;TZID=Europe/Brussels:20140328T140000
DTSTAMP:20140304T044544Z
LOCATION:NO Solvay (5th floor)
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=NO Solvay (5th floor):
SEQUENCE:7
DESCRIPTION:Title:\nOn the Boundedness Problem for Pushdown Vector Addit
ion Systems\n\nAbstract:\nVector addition systems (VAS)\, or equivalentl
y Petri nets\, are a well-studied and fundamental model for the analysis
of concurrent systems. Despite their fairly large expressive power\, ma
ny verification problems for VAS are decidable: coverability\, boundedne
ss\, reachability\, liveness\, etc. In this work\, we study an extension
of VAS\, called Pushdown VAS\, that allows them to use a stack over a f
inite alphabet. Our main contribution is an algorithm for the boundednes
s problem together with an analysis of its complexity. This algorithm is
based on the well-known Karp-Miller tree for VAS. We show that the wors
t-case running time of this algorithm is hyper- Ackermannian. (Joint wor
k with G. Sutre and M. Praveen)
END:VEVENT
BEGIN:VEVENT
CREATED:20180316T112951Z
UID:9C4BFFF9-04E3-4344-8E8B-FF580D95FF3E
DTEND;TZID=Europe/Brussels:20180511T153000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Diego Figueira (LaBRI)
DTSTART;TZID=Europe/Brussels:20180511T140000
DTSTAMP:20180316T113026Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
END:VEVENT
BEGIN:VEVENT
CREATED:20140110T150725Z
UID:26772B2A-26C4-4B9F-84BA-B7461A1DC2C3
DTEND;TZID=Europe/Brussels:20140328T163000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Mahsa Shirmohammadi (ULB & LSV - ENS Cachan)
DTSTART;TZID=Europe/Brussels:20140328T160000
DTSTAMP:20140304T044515Z
LOCATION:NO Solvay (5th floor)
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-TITLE=NO Solvay (5th floor):
SEQUENCE:11
DESCRIPTION:Title: Limit Synchronization in Markov Decision Processes\n
\nAbstract: Markov decision processes (MDP) are finite-state systems wit
h both strategic and probabilistic choices. After fixing a strategy\, an
MDP produces a sequence of probability distributions over states. The s
equence is eventually synchronizing if the probability mass accumulates
in a single state\, possibly in the limit. Precisely\, for 0 ≤ p ≤ 1 the
sequence is p-synchronizing if a probability distribution in the sequen
ce assigns probability at least p to some state\, and we distinguish thr
ee synchronization modes: (i) sure winning if there exists a strategy th
at produces a 1-synchronizing sequence\; (ii) almost-sure winning if the
re exists a strategy that produces a sequence that is\, for all ε > 0\,
a (1-ε)-synchronizing sequence\; (iii) limit-sure winning if for all ε >
0\, there exists a strategy that produces a (1-ε)-synchronizing sequenc
e. In this talk\, we consider the problem of deciding whether an MDP is
sure\, almost-sure\, or limit-sure inning\, and we present some results
about the computational complexity of these decision problems and memory
requirement for optimal winning strategies.
END:VEVENT
BEGIN:VEVENT
CREATED:20150105T160435Z
UID:3A536710-7242-471D-98C0-4C1592C74FEF
DTEND;TZID=Europe/Brussels:20150123T163000
TRANSP:OPAQUE
SUMMARY:[cfv] Mickael Randour
DTSTART;TZID=Europe/Brussels:20150123T160000
DTSTAMP:20150105T160435Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Percentile Queries in Multi-Dimensional Markov Decisi
on Processes\n\nAbstract:\nMarkov decision processes (MDPs) with multi-d
imensional weights are useful to analyze systems with multiple objective
s that may be conflicting and require the analysis of trade-offs. In thi
s work\, we study the complexity of percentile queries in such MDPs and
give algorithms to synthesize strategies that enforce such constraints.
Given a multi-dimensional weighted MDP and a quantitative payoff functio
n~$f$\, thresholds $v_i$ (one per dimension)\, and probability threshold
s $\\alpha_i$\, we show how to compute a single strategy to enforce that
for all dimensions $i$\, the probability of outcomes $\\rho$ satisfying
$f_i(\\rho) \\geq v_i$ is at least $\\alpha_i$. We consider classical q
uantitative payoffs from the literature (sup\, inf\, lim sup\, lim inf\,
mean-payoff\, truncated sum\, discounted sum). Our work extends to the
quantitative case the multi-objective model checking problem studied by
Etessami et al. in unweighted MDPs. Joint work with Jean-François Raskin
and Ocan Sankur.
END:VEVENT
BEGIN:VEVENT
CREATED:20140501T094156Z
UID:0D596982-38F2-4661-8CDB-B9699E9FB3E4
DTEND;TZID=Europe/Brussels:20140516T153000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Florent Jacquemard (IRCAM)
DTSTART;TZID=Europe/Brussels:20140516T140000
DTSTAMP:20140501T094430Z
LOCATION:Forum D
SEQUENCE:7
DESCRIPTION:Title: Timed Verification and Testing of an Interactive Musi
c System\n\nAbstract: \nInteractive Music Systems are involved in live p
erformances with human musicians. They react in real time to audio signa
ls and asynchronous incoming events according to a pre-specified timed s
cenario called a mixed score\, written in a domain specific language (DS
L). They are expected to act in a reliable way\, be robust to environme
ntal changes\, unforeseen errors in input and have a predictable behavio
r\, in particular regarding timings.\nFollowing these strong requirement
s\, as much efforts as possible must be taken to assess before a perform
ance that their behavior will conform to expectations\, for a given mixe
d score\, at a level of exhaustiveness that cannot be reached during reh
earsals with musicians.\nIn this talk we will see the application of som
e formal methods to evaluation of an IMS called Antescofo\, developed at
Ircam and used regularly in concerts worldwide.\nWe will introduce Ante
scofo’s DSL and an medium-level intermediate representation (IR) of mixe
d scores. Then we will present various verification and testing tasks ba
sed on timed automata models derived from the IR:\n* model based conform
ance testing\,\n* the evaluation of the robustness of mixed scores to th
e timing variations in human performances\, \n* schedulability analysis.
BEGIN:VALARM
X-WR-ALARMUID:B90A78EA-1092-45AA-9580-000F789E582B
UID:B90A78EA-1092-45AA-9580-000F789E582B
TRIGGER;VALUE=DATE-TIME:19760401T005545Z
ACTION:NONE
END:VALARM
BEGIN:VALARM
X-WR-ALARMUID:05ACA425-381C-468C-9343-BE9CAF079E4F
UID:05ACA425-381C-468C-9343-BE9CAF079E4F
TRIGGER:-P1W
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
END:VALARM
END:VEVENT
BEGIN:VEVENT
TRANSP:OPAQUE
DTEND;TZID=Europe/Brussels:20140606T153000
UID:C625780D-8D06-48CB-9A8F-DC903CE54A30
DTSTAMP:20140501T094642Z
LOCATION:Room 2NO9.06
DESCRIPTION:Title: Two classes of infinite duration games\n\nAbstract: D
uring this talk\, I discuss two classes of infinite duration games that
are related to each other. I give an overview of the main questions and
results\, recent developments\, and also a bit of the underlying techniq
ues. I devote special attention to the zero-sum case (i.e. when there ar
e only two players and they have completely opposite interests).\n\nI co
nsider games that are played on a state space (think of positions) by a
number of players. At time period 1\, the play of the game is in an init
ial state\, where each player has to choose an action from a given actio
n set. These choices are made simultaneously and independently. Then\, a
ccording to a probability distribution that depends on the chosen action
s and the state\, the play moves to a new state. At time period 2\, in t
he new state\, the players choose actions again\, and so on. This is rep
eated infinitely long.\n\nIn the first class of games\, the players rece
ive an instantaneous reward at every time period\, as a function of the
actions and the current state at that time period. Each player's goal is
then to maximize his/her long-term average reward. \n\nIn the second cl
ass of games\, it is assumed that in every state\, only one player has m
ore than one action (the interpretation is that this player controls the
state). But the evaluation of the play is very general\, that is\, each
player is given a payoff function that assigns a real number to each in
finite sequence of states and actions that can arise by playing the game
. Then\, his/her goal is to maximize this payoff function. \n\nDuring th
is talk\, we are mainly interested in the following solution concepts: (
approximately) optimal strategies in the zero-sum case\, and (approximat
e) Nash or subgame-perfect equilibria in the general case (so the non-ze
ro-sum case).
STATUS:CONFIRMED
SEQUENCE:10
SUMMARY:[cfv seminar] János Flesch (Maastricht University)
LAST-MODIFIED:20140417T143408Z
DTSTART;TZID=Europe/Brussels:20140606T140000
CREATED:20140417T143408Z
BEGIN:VALARM
X-WR-ALARMUID:F16BA35B-6498-4921-984E-9597B11FAA14
UID:F16BA35B-6498-4921-984E-9597B11FAA14
TRIGGER:P1W
ACTION:EMAIL
ATTENDEE:mailto:gaperez64@gmail.com
SUMMARY:Alarm notification
DESCRIPTION:This is an event reminder
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20140507T131419Z
UID:FC334F86-4EAC-45E6-8BC6-97CA782A86CB
DTEND;TZID=Europe/Brussels:20140516T160000
TRANSP:OPAQUE
SUMMARY:[cfv seminar] Emmanuel Filiot (ULB)
DTSTART;TZID=Europe/Brussels:20140516T153000
DTSTAMP:20140507T131513Z
SEQUENCE:8
DESCRIPTION:Title: From Two-Way to One-Way Finite State Transducers\n\nA
bstract:\nAny two-way finite state automaton is equivalent to some one-w
ay finite state automaton. This well-known result\, shown by Rabin and S
cott and independently by Shepherdson\, states that two-way finite state
automata (even non-deterministic) characterize the class of regular lan
guages. It is also known that this result does not extend to finite stri
ng transductions: (deterministic) two-way finite state transducers stric
tly extend the expressive power of (functional) one-way transducers. In
particular deterministic two-way transducers capture exactly the class o
f MSO-transductions of finite strings. In this paper\, we address the fo
llowing definability problem: given a function defined by a two-way fini
te state transducer\, is it definable by a one-way finite state transduc
er? By extending Rabin and Scott's proof to transductions\, we show that
this problem is decidable. Our procedure builds a one-way transducer\,
which is equivalent to the two-way transducer\, whenever one exists.
END:VEVENT
BEGIN:VEVENT
CREATED:20151206T125453Z
UID:1F981912-E119-478F-A355-ABC52481EBFB
DTEND;TZID=America/Chicago:20160226T093000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Nathan Lhote (Labri\, ULB)
DTSTART;TZID=America/Chicago:20160226T090000
DTSTAMP:20160127T090944Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Towards an algebraic theory of rational word function
s\n\nAbstract:\nIn formal language theory\, several different models cha
racterize regular languages\, such as finite automata\, congruences of f
inite index\, or monadic second-order logic (MSO). Moreover\, several fr
agments of MSO have effective characterizations based on algebraic prope
rties. When we consider transducers instead of automata\, such character
izations are much more challenging\, because many of the properties of r
egular languages do not generalize to regular word functions. \n\nIn thi
s paper we consider word functions that are definable by one-way transdu
cers (rational functions). We show that the canonical bimachine of Reute
nauer and Schützenberger preserves certain algebraic properties of ratio
nal functions\, similar to the case of word languages. In particular\, w
e give an effective characterization of functions that can be defined by
an aperiodic one-way transducer.
END:VEVENT
BEGIN:VEVENT
CREATED:20180316T113031Z
UID:118D935A-CDD7-4BA9-902E-662466218271
DTEND;TZID=Europe/Brussels:20180511T113000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Elham Kashefi (U. of Edinburgh): Verification of quantum c
omputation
DTSTART;TZID=Europe/Brussels:20180511T100000
DTSTAMP:20180316T113031Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
DESCRIPTION:Abstract: Quantum computers promise to efficiently solve not
only problems believed to be intractable for classical computers\, but
also problems for which verifying the solution is also considered intrac
table. This raises the question of how one can check whether quantum com
puters are indeed producing correct results. This task\, known as quantu
m verification\, has been highlighted as a significant challenge on the
road to scalable quantum computing technology. We review the most signif
icant approaches to quantum verification and compare them in terms of st
ructure\, complexity and required resources. We also comment on the use
of cryptographic techniques which\, for many of the presented protocols\
, has proven extremely useful in performing verification. Finally\, we d
iscuss issues related to fault tolerance\, experimental implementations
and the outlook for future protocols.
END:VEVENT
BEGIN:VEVENT
CREATED:20141112T131635Z
UID:9585FF89-825D-479A-AC97-D45ADDC31DDF
DTEND;TZID=Europe/Brussels:20141128T163000
TRANSP:OPAQUE
SUMMARY:[cfv] Isabelle Mainz
DTSTART;TZID=Europe/Brussels:20141128T160000
DTSTAMP:20141112T131635Z
LOCATION:ULB - Forum D
SEQUENCE:0
DESCRIPTION:Title:\nAcceleration of affine hybrid transformations\n\nAbs
tract:\nIn this talk I will speak about the computation of the set of re
achable configurations of linear hybrid automata. The approach relies on
symbolic state-space exploration\, using acceleration in order to speed
up the computation and to make it terminate for a broad class of system
s. I will present an original method for accelerating the control cycles
of linear hybrid automata\, i.e.\, to compute their unbounded repeated
effect. The idea consists in analyzing the data transformations that lab
el these cycles\, by reasoning about the geometrical features of the cor
responding system of linear constraints. This approach is complete over
Multiple Counters Systems (MCS)\, and is able to accelerate hybrid trans
formations that are out of scope of existing techniques.
END:VEVENT
BEGIN:VEVENT
CREATED:20141103T083225Z
UID:92E33105-6901-4FDF-A22D-05B9DC6F54AF
DTEND;TZID=Europe/Brussels:20141128T153000
TRANSP:OPAQUE
SUMMARY:[cfv] Ahmed Bouajjani
DTSTART;TZID=Europe/Brussels:20141128T140000
DTSTAMP:20141103T083225Z
LOCATION:ULB - Forum D
SEQUENCE:0
DESCRIPTION:Title:\nTractable Refinement Checking for Concurrent Objects
\n\nAbstract:\nEfficient implementations of concurrent objects such as s
emaphores\, locks\,\nand atomic collections are essential to modern comp
uting. Yet programming\nsuch objects is error prone: in minimizing the s
ynchronization overhead\nbetween concurrent object invocations\, one ris
ks the conformance to\nreference implementations --- or in formal terms\
, one risks violating\n"observational refinement". Testing this refineme
nt even within a\nsingle execution is intractable\, limiting existing ap
proaches to executions\nwith very few object invocations.\n\nWe develop
a polynomial-time (per execution) approximation to\nrefinement checking.
The approximation is parameterized by an accuracy $k$ (a natural number
)\nrepresenting the degree to which refinement violations are\nvisible.
In principle\, more violations are detectable as $k$ increases\, and\nin
the limit\, all are detectable. Our insight for this approximation aris
es\nfrom foundational properties on the partial orders characterizing th
e\nhappens-before relations between object invocations: they are\n"inter
val orders"\, with a well defined measure of complexity\,\ni.e.\,~their
"length". Approximating the happens-before relation with a\npossibly-wea
ker interval order of bounded length can be efficiently\nimplemented by
maintaining a bounded number of integer counters. In\npractice\, we find
that refinement violations can be detected with very\nsmall values of $
k$\, and that our approach scales far beyond existing\nrefinement-checki
ng approaches.\n\nThis is a joint work with Michael Emmi\, Constantin En
ea\, and Jad Hamza.
END:VEVENT
BEGIN:VEVENT
CREATED:20141112T131829Z
UID:A2710335-F15A-4155-AB44-20E949C90853
DTEND;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:20150
227T153000
TRANSP:TRANSPARENT
SUMMARY:[cfv] Mikołaj Bojańczyk
DTSTART;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:201
50227T140000
DTSTAMP:20141112T131829Z
SEQUENCE:2
LOCATION:NO Solvay (5th floor)
DESCRIPTION:Title: Transducers with origin information\n\nAbstract:\nA t
ransducer with origin information inputs a word\, and produces not just
an output word\, but also a mapping from positions of the output word to
positions of the input word. This mapping is called the origin informat
ion. For instance\, over a one letter input alphabet\, the identity func
tion and the reverse function are the same functions without origin info
rmation\, but are different functions with origin information. I will ar
gue that having origin information in the semantics makes the theory of
transducers easier and perhaps better behaved.
CLASS:PUBLIC
LAST-MODIFIED:20150212T201314Z
BEGIN:VALARM
X-WR-ALARMUID:310C896C-DC43-4EED-911B-DCECE5811F41
UID:310C896C-DC43-4EED-911B-DCECE5811F41
TRIGGER;VALUE=DURATION:-PT15H
X-APPLE-DEFAULT-ALARM:TRUE
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
X-EVOLUTION-ALARM-UID:20150212T200332Z-1965-1000-1-8@localhost.localdoma
in
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20141201T184123Z
UID:5CEE4F80-14B5-4273-A3C7-A3753BF58D59
DTEND;TZID=Europe/Brussels:20141212T163000
TRANSP:OPAQUE
SUMMARY:[cfv] Ocan Sankur
DTSTART;TZID=Europe/Brussels:20141212T160000
DTSTAMP:20141201T184123Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title:\nMultiple-Environment Markov Decision Processes\n\nAb
stract:\nWe introduce Multi-Environment Markov Decision Processes (MEMDP
s) which are MDPs with a set of probabilistic transition functions. The
goal in a MEMDP is \nto synthesize a single controller with guaranteed p
erformances against all \nenvironments even though the environment is un
known a priori. While MEMDPs can be seen as a special class of partially
observable MDPs\, we show that several \nverification problems that are
undecidable for partially observable MDPs\, are decidable for MEMDPs an
d sometimes have even efficient solutions.
END:VEVENT
BEGIN:VEVENT
CREATED:20141209T152829Z
UID:06EECEE6-C5F8-4B67-985C-32856F626519
DTEND;TZID=Europe/Brussels:20141212T153000
TRANSP:OPAQUE
SUMMARY:[cfv] Arnaud Sangnier
DTSTART;TZID=Europe/Brussels:20141212T140000
DTSTAMP:20141209T152829Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title:\nParameterized Reachability in Networks with Many Ide
ntical Processes\n\nAbstract:\nIn this talk\, we will study the decidabi
lity and complexity of reachability problems in networks where the numbe
r of entities is a priori unknown but where each process follows the sam
e behavior. I will first describe algorithmic methods to analyze such ne
tworks considering different means of communication between the processe
s such as rendez-vous communication (with or without a central controlle
r)\, broadcast communication or reconfigurable broadcast communication (
where the broadcast messages are not received by all the processes of th
e networks). I will then present some considerations on how local strate
gies can be considered in such networks and I will end by providing som
e future research directions for the field of parameterized verification
s motivated by concrete examples.
END:VEVENT
BEGIN:VEVENT
CREATED:20141210T084523Z
UID:64486B47-8C6C-4D5D-89B2-A89B2A00B82B
DTEND;TZID=Europe/Brussels:20150123T153000
TRANSP:OPAQUE
SUMMARY:[cfv] Joost-Pieter Katoen
DTSTART;TZID=Europe/Brussels:20150123T140000
DTSTAMP:20141107T084711Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Safety and Liveness -- New Results and Perspectives\n
\nAbstract:\nLamport’s notions of safety and liveness properties are fol
klore. Safety says that nothing wrong happens whereas liveness ensures t
hat progress is made. Since the 1980s\, several formalizations and vari
ations have been investigated.\n\nThis talk presents some new developmen
ts on this classical property classification. This includes new results
for LTL\, for Markov chains and timed automata. We present a sound and
complete characterization of safety in probabilistic CTL — every safe PC
TL formula is a safety property and every safety property (expressible i
n PCTL) can be expressed in safe PCTL. The same holds for liveness\, bu
t this necessarily resorts on satisfiability checking.\n\nFor timed syst
ems we provide a topological characterisation of branching-time real-tim
e safety and liveness properties and give sound and complete fragments o
f timed CTL. We show that deciding whether a TCTL-formula is safety or
liveness is in general undecidable. We discuss how a (finitely branchin
g) timed CTL formula can be decomposed into the conjunction of a safety
and a liveness property\, both represented by timed alternating tree aut
omata.
END:VEVENT
BEGIN:VEVENT
CREATED:20141112T131809Z
UID:287EF079-6CBB-4346-84AE-530E57369188
DTEND;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:20150
227T113000
TRANSP:TRANSPARENT
SUMMARY:[cfv] Christof Löding
DTSTART;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:201
50227T100000
DTSTAMP:20141112T131809Z
SEQUENCE:2
LOCATION:NO Solvay (5th floor)
DESCRIPTION:Title: Synthesis of Transducers from Automatic Specification
s\n\nAbstract:\nGiven a specification as a binary relation that relates
inputs to admissible outputs\, the synthesis problem asks for a program
that produces for each input an output that is admissible according to t
he specification. We consider this problem over the domain of words and
trees. The specifications are given by automatic relations\, that is\, r
elations that can be defined by finite automata that read pairs of struc
tures and accept those pairs that are in the relation. For such specific
ations\, we study the synthesis problem of deterministic finite state tr
ansducers. In particular\, we present some recent results and ongoing wo
rk on the synthesis of tree transducers.
CLASS:PUBLIC
LAST-MODIFIED:20150212T200849Z
BEGIN:VALARM
X-WR-ALARMUID:6E3B60DB-7A71-483D-882B-28288AF8E3EB
UID:6E3B60DB-7A71-483D-882B-28288AF8E3EB
TRIGGER;VALUE=DURATION:-PT15H
X-APPLE-DEFAULT-ALARM:TRUE
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
X-EVOLUTION-ALARM-UID:20150212T200332Z-1965-1000-1-6@localhost.localdoma
in
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20160510T074209Z
UID:9FAE97D0-2C21-49A9-8B41-A36D8675D1EC
DTEND;TZID=Europe/Brussels:20160520T153000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Pierre-Alain Reynier
DTSTART;TZID=Europe/Brussels:20160520T140000
DTSTAMP:20160510T074209Z
LOCATION:Forum H (ULB\, La Plaine)
SEQUENCE:0
DESCRIPTION:Survey on transducers of (nested) words: decidability\, logi
c and algebra\n\nAbstract: Algorithmic formal verification has proved to
be a promising technology to improve reliability and quality of softwar
e systems. These works are rooted in the theory of regular languages\, t
hat enjoy important automata-logic-algebra connections. In order to addr
ess software systems realizing input/output transformations (such as edi
tion\, pattern replacement\, refactorization…)\, the model of word-to-wo
rd transducers appears as a natural candidate. Fundamental problems conc
erning transducers include equivalence\, type checking\, closure under c
omposition\, but also determinisation and minimisation.\nThis talk will
provide a survey about transducers\, and more precisely (if time permits
):\n\ni) decidability results based on patterns\, that allow to derive e
fficient decision procedures\,\n\nii) logic and algebra connections\,\n\
niii) extensions to nested words.
END:VEVENT
BEGIN:VEVENT
CREATED:20150121T102353Z
UID:7119C6BC-6C8E-478B-AE49-21D4E10F4D30
DTEND;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:20150
227T121500
TRANSP:TRANSPARENT
SUMMARY:[cfv] Emmanuel Filiot
DTSTART;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:201
50227T114500
DTSTAMP:20150121T102353Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:2
LAST-MODIFIED:20150212T201159Z
CLASS:PUBLIC
DESCRIPTION:Title: Finite-Valued Weighted Automata\n\nAbstract:\nAny wei
ghted automaton (WA) defines a relation from finite words to values: giv
en an input word\, its set of values is obtained as the set of values co
mputed by each accepting run on that word. A WA is k-valued if the relat
ion it defines has degree at most k\, i.e.\, every set of values associa
ted with an input word has cardinality at most k. We investigate the cla
ss of quantitative languages defined by k-valued automata\, for all para
meters k. We consider several measures to associate values with runs: su
m\, discounted-sum\, and more generally values in groups. We define a ge
neral procedure which decides\, given a bound k and a WA over a group\,
whether this automaton is k-valued. We also show that any k-valued WA ov
er a group\, under some general conditions\, can be decomposed as a unio
n of k unambiguous WA. While inclusion and equivalence are undecidable p
roblems for arbitrary sum-automata\, we show\, based on this decompositi
on\, that they are decidable for k-valued sum-automata\, and k-valued di
scounted sum automata over inverted integer discount factors. We finally
show that the quantitative Church problem is undecidable for k-valued s
um-automata\, even given as finite unions of deterministic sum-automata.
BEGIN:VALARM
X-WR-ALARMUID:8C8277DD-E9CC-4A39-A6C2-1E46C8DB0E39
UID:8C8277DD-E9CC-4A39-A6C2-1E46C8DB0E39
TRIGGER;VALUE=DURATION:-PT15H
X-APPLE-DEFAULT-ALARM:TRUE
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
X-EVOLUTION-ALARM-UID:20150212T200332Z-1965-1000-1-7@localhost.localdoma
in
END:VALARM
END:VEVENT
BEGIN:VEVENT
UID:20150212T201324Z-10539-1000-1715-52@localhost.localdomain
DTSTAMP:20150212T200249Z
DTSTART;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:201
50227T160000
DTEND;TZID=/freeassociation.sourceforge.net/Tzfile/Europe/Brussels:20150
227T163000
TRANSP:OPAQUE
SEQUENCE:3
SUMMARY:[cfv] Guillermo A. Pérez
LOCATION:NO Solvay (5th floor)
CLASS:PUBLIC
DESCRIPTION:Title: Reactive Synthesis Without Regret\n\nAbstract:\nTwo-p
layer\, zero-sum games of infinite duration and their quantitative gener
alizations are often used in verification to model the interaction betwe
en a controller (Eve) and an antagonistic environment (Adam). The questi
on usually addressed is that of the existence (and computability) of a s
trategy for Eve that can win against any strategy of Adam. In this work
we are interested in strategies of Eve that minimize her regret as defin
ed by Halpern and Pass. We give algorithms to compute the strategies of
Eve that ensure minimal regret against an adversary whose choice of stra
tegy is (i) unrestricted\, (ii) limited to positional strategies\, or (i
ii) limited to word strategies.
CREATED:20150212T201602Z
LAST-MODIFIED:20150212T201602Z
END:VEVENT
BEGIN:VEVENT
CREATED:20150223T090951Z
UID:5B353418-BE6D-4442-A2F5-57C9BC34A9B2
DTEND;TZID=Europe/Brussels:20150320T163000
TRANSP:OPAQUE
SUMMARY:[cfv] Romain Brenguier
DTSTART;TZID=Europe/Brussels:20150320T160000
DTSTAMP:20150223T090951Z
LOCATION:TBA
SEQUENCE:0
DESCRIPTION:Title: Assume-Admissible Synthesis\n\nAbstract:\nWe introduc
e a novel rule for synthesis of reactive systems\, applicable to systems
made of n components which have each their own objectives. It is based
on the notion of admissible strategies. We compare our novel rule with p
revious rules defined in the literature\, and we show that contrary to t
he previous proposals\, our rule define sets of solutions which are rect
angular. This property leads to solutions which are robust and resilient
. We provide complete algorithms with optimal complexity and also an abs
traction framework which allows us to define necessary conditions to com
pute compositionally sets of winning assume-admissible strategies for ea
ch player in the game.
END:VEVENT
BEGIN:VEVENT
CREATED:20160413T114245Z
UID:A4479819-3065-4808-B5AD-4909297A3606
DTEND;TZID=Europe/Brussels:20160422T153000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Javier Esparza (TUM)
DTSTART;TZID=Europe/Brussels:20160422T140000
DTSTAMP:20160413T114245Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Verification of population protocols\n\nAbstract:\nPopulatio
n protocols (Angluin et al.\, 2006) are a formal model of sensor\nnetwor
ks consisting of identical mobile devices. When two devices come into th
e\nrange of each other\, they interact and change their states. Computat
ions are\ninfinite sequences of pairwise interactions where the interact
ing processes\nare picked by a fair scheduler.\n\nA population protocol
is well-specified if for every initial configuration C\nof devices\, and
every computation starting at C\, all devices eventually agree\non a co
nsensus value depending only on C. If a protocol is well-specified\,\nth
en it is said to compute the predicate that assigns to each initial\ncon
figuration its consensus value.\n\nWhile the predicates computable by we
ll-specified protocols have been\nextensively studied\, the two basic ve
rification problems remain open: is a\ngiven protocol well-specified? Do
es a protocol compute a given predicate?\nIn the first part of the talk
we study these problems.\nIn the second part we discuss the more general
question of checking\nif a population protocol with a random scheduler
satisfies a PLTL property.
END:VEVENT
BEGIN:VEVENT
CREATED:20160511T201312Z
UID:6F7C4921-F820-4878-A5A9-4CC9D5A87EC1
DTEND;TZID=Europe/Brussels:20160520T163000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Ismaël Jecker (ULB)
DTSTART;TZID=Europe/Brussels:20160520T160000
DTSTAMP:20160511T201624Z
LOCATION:Forum H (ULB\, La Plaine)
SEQUENCE:0
DESCRIPTION:On Equivalence and Uniformisation Problems for Finite Transd
ucers\n\nAbstract:\nTransductions are binary relations of finite words.
For rational transductions\,\ni.e.\, transductions defined by finite tra
nsducers\, the inclusion\, equivalence and sequential uniformisation pro
blems are known to be undecidable. We investigate stronger variants of i
nclusion\, equivalence and sequential uniformisation\, based on a genera
l notion of transducer resynchronisation\, and show their decidability.\
n\nWe also investigate the classes of finite-valued rational transductio
ns and deterministic rational transductions\, which are known to have a
decidable equivalence problem. We show that sequential uniformisation i
s also decidable for them.
END:VEVENT
BEGIN:VEVENT
CREATED:20180122T090251Z
UID:00085AFB-2A31-4DF1-9ACC-FE98429C583A
DTEND;TZID=Europe/Brussels:20180330T153000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Jan Kretinsky (TU Munich): Fast Learning of Small Strategi
es
DTSTART;TZID=Europe/Brussels:20180330T140000
DTSTAMP:20180122T090251Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
DESCRIPTION:In verification\, precise analysis is required\, but the alg
orithms usually suffer from scalability issues. In machine learning\, sc
alability is achieved\, but with only very weak guarantees. We show how
to merge the two philosophies and profit from both. \n\nIn this talk\, w
e discuss models such as Markov decision processes\, two-player games\,
stochastic games\, and objectives such as reachability\, LTL\, mean payo
ff.\n\nWe show how to learn ε-optimal strategies fast and how to represe
nt them concisely so that some understanding of the behaviour and debugg
ing information can be extracted.
END:VEVENT
BEGIN:VEVENT
CREATED:20150223T091104Z
UID:03D8E209-20FA-41D8-ACAC-E4E707016310
DTEND;TZID=Europe/Brussels:20150320T153000
TRANSP:OPAQUE
SUMMARY:[cfv] Patricia Bouyer-Decitre
DTSTART;TZID=Europe/Brussels:20150320T140000
DTSTAMP:20150223T091104Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: On the optimal reachability problem in weighted timed
games\n\nAbstract:\nA weighted timed game is a timed game with extra qu
antitative information representing e.g. energy consumption. Optimizing
the weight for reaching a target is a natural question\, which has been
investigated for ten years. Existence of optimal strategies is known to
be undecidable in general\, and only very restricted classes of games ha
ve been described for which optimal weight and almost-optimal strategies
can be computed. \nIn this talk\, I will give an overview of rather old
results about the optimal reachability problem in weighted timed automa
ta and games. I will then focus on more recent results\, that are joint
work with Samy Jaziri and Nicolas Markey. First I will show that the val
ue problem is undecidable in weighted timed games. I will then describe
an algorithm to compute arbitrary approximations of the value in a game\
, and corresponding almost-optimal strategies. The algorithm applies to
a large subclass of weighted timed games\, and is the first approximatio
n scheme which is designed in the current context.
END:VEVENT
BEGIN:VEVENT
CREATED:20160212T092151Z
UID:C7FA39E6-685E-48C6-8EE5-FB68D14EFD67
DTEND;TZID=America/Chicago:20160226T051500
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Pierre Carlier (UMons)
DTSTART;TZID=America/Chicago:20160226T044500
DTSTAMP:20160220T115204Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Decisiveness and stochastic timed automata\n\nAbstrac
t: In 2007\, Abdulla et al introduced the elegant concept of decisive Ma
rkov chain w.r.t. a given target set F. Intuitively\, the concept of dec
isiveness allows to lift the good properties of finite Markov chains to
infinite Markov chains. For instance\, the approximate quantitative safe
ty problem can be solved for decisive Markov chains (enjoying reasonable
effectiveness assumptions) including PLCS and PVASS. In this paper\, we
extend the concept of decisiveness to more general stochastic processes
. This extension is non trivial as we consider stochastic processes with
a potentially continuous set of states and uncountable branching (commo
n features of continuous-time stochastic process). This allow us to obta
in decidability results for both qualitative and quantitative verificati
on problems on continuous-time stochastic process\, including GSMP and S
TA.\n\nThis is a joint work with Nathalie Bertrand\, Patricia Bouyer and
Thomas Brihaye.
END:VEVENT
BEGIN:VEVENT
CREATED:20160416T111625Z
UID:32BFD966-8817-47BB-8C93-AA55B9D11BA7
DTEND;TZID=Europe/Brussels:20160422T163000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Guillermo A. Pérez (ULB)
DTSTART;TZID=Europe/Brussels:20160422T160000
DTSTAMP:20160416T111813Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Admissibility in Quantitative Graph Games\n\nAbstract
:\nThe notion of admissible strategy has been proposed in game theory to
formalize rationality of players. It has been studied recently for game
s of infinite duration with Boolean objectives. In this paper\, we exten
d this study to games of infinite duration with quantitative objectives.
First\, we show that\, under the assumption that optimal worst-case and
cooperative strategies exist\, admissible strategies are guaranteed to
exist. Second\, we give a characterization of admissible strategies usin
g the notion of adversarial and cooperative values of a history\, and we
characterize the set of outcomes that are compatible with admissible st
rategies. Finally\, we show how these characterizations can be used to d
esign algorithms to decide verification and synthesis problems related t
o the notion of admissible strategy.
END:VEVENT
BEGIN:VEVENT
CREATED:20180223T092111Z
UID:22B64D56-37D8-46DF-A62F-1C6321C96844
DTEND;TZID=Europe/Brussels:20180330T113000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Luc de Raedt (KU Leuven): Probabilistic logic programming
and its applications
DTSTART;TZID=Europe/Brussels:20180330T100000
DTSTAMP:20180223T092111Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
DESCRIPTION:Probabilistic programs combine the power of programming lang
uages with that of probabilistic graphical models. There has been a lot
of progress in this paradigm over the past twenty years. This talk will
introduce probabilistic logic programming languages\, which are based on
Sato's distribution semantics and which extend probabilistic databases.
The key idea is that facts or tuples can be annotated with probabilitie
s that indicate their degree of belief. Together with the rules that enc
ode domain knowledge they induce a set of possible worlds. After an intr
oduction to probabilistic programs\, which will cover semantics\, infere
nce\, and learning\, the talk will sketch some emerging applications in
knowledge based systems\, in cognitive robotics and in answering probabi
lity questions.
END:VEVENT
BEGIN:VEVENT
CREATED:20151215T151346Z
UID:3CD1EF12-CFFE-425D-8511-CE82AD2CC24F
DTEND;TZID=America/Chicago:20160129T083000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Nicolas Markey (LSV / CNRS & ENS Cachan)
DTSTART;TZID=America/Chicago:20160129T070000
DTSTAMP:20151215T151346Z
LOCATION:P.2NO9.06 (La Plaine)
SEQUENCE:0
DESCRIPTION:Title: Temporal logics for multi-player games\n\nAbstract:\n
The alternating-time temporal logic (ATL) was defined 15 years ago as an
extension of CTL for expressing and verifying properties of multi-playe
r games. However\, in order to inherit nice algorithmic properties of CT
L\, ATL has limited expressiveness: it cannot really express strategic i
nteractions between several players. In this talk\, I will present our e
xtension of ATL with strategy contexts\, which contrary to ATL can expre
ss rich properties with interactions between strategies (e.g. equilibria
properties). I will then present our results about model checking and s
atisfiability for this logic\, using quantified CTL as an intermediary t
ool. This talk is based on joint works with Thomas Brihaye\, Arnaud Da C
osta Lopes\, and François Laroussinie.
END:VEVENT
BEGIN:VEVENT
CREATED:20151202T170513Z
UID:16B33F11-0B81-476A-94C5-339E471D3FC9
DTEND;VALUE=DATE:20160403
TRANSP:TRANSPARENT
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] CASSTING 2016: Workshop on Games for the Synthesis of Comp
lex Systems
DTSTART;VALUE=DATE:20160402
DTSTAMP:20151202T170626Z
LOCATION:Eindhoven\, NL - colocated with ETAPS 2016
SEQUENCE:0
DESCRIPTION:Website: http://www.etaps.org/index.php/2016/workshops
BEGIN:VALARM
X-WR-ALARMUID:1D468E09-4B6E-44A0-8E17-D2315D906402
UID:1D468E09-4B6E-44A0-8E17-D2315D906402
TRIGGER:-PT15H
X-APPLE-DEFAULT-ALARM:TRUE
ATTACH;VALUE=URI:Basso
ACTION:AUDIO
END:VALARM
END:VEVENT
BEGIN:VEVENT
CREATED:20151126T121039Z
UID:3C1140EC-3CA9-44D5-B21B-AA6711562763
DTEND;TZID=America/Chicago:20160226T043000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Philippe Schnoebelen (LSV / CNRS & ENS Cachan)
DTSTART;TZID=America/Chicago:20160226T030000
DTSTAMP:20151206T125345Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Well-Structured Systems: Algorithms and Complexity\n\
nAbstract: Well-structured systems\, aka WSTS\, are a family of infinite
-state computational models that support generic decidability results ba
sed on well-quasi-ordering theory. They have many applications in logics
of programs and verification.
END:VEVENT
BEGIN:VEVENT
CREATED:20151126T121046Z
UID:82930630-E3A2-4D54-859E-781B9DDD2270
DTEND;TZID=America/Chicago:20160226T083000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Parosh Aziz Abdulla (Uppsala)
DTSTART;TZID=America/Chicago:20160226T070000
DTSTAMP:20151206T125424Z
LOCATION:NO Solvay (5th floor)
SEQUENCE:0
DESCRIPTION:Title: Automatic Verification of Linearizability \n\nAbstrac
t:\nWe consider the problem of proving linearizability for concurrent t
hreads that access a shared data structure. Such systems give rise to
unbounded numbers of threads that operate on an bounded data domain and
that access dynamically allocated memory. Furthermore\, proving lineariz
ability is harder than proving control state reachability due to existen
tially quantified linearization points. The problem is further complicat
ed by the presence of advanced features such as non-fixed linearization
points\, speculation\, and helping. In this presentation\, we present a
framework that can automatically verify linearizability for concurrent
data structures that implement sets\, stacks\, and queues. We use a spec
ification formalism for linearization techniques which allows the user t
o specify\, in a simple and and concise manner\, complex patterns includ
ing non-fixed linearization points. Then\, we define abstraction techniq
ues that allow to make the size of the data domain and the number of th
reads finite.
END:VEVENT
BEGIN:VEVENT
CREATED:20151220T132517Z
UID:5571C9B4-648F-4655-9F4E-41DFAB68C15D
DTEND;TZID=Europe/Brussels:20160129T163000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Stéphane Le Roux (ULB)
DTSTART;TZID=Europe/Brussels:20160129T160000
DTSTAMP:20151220T132517Z
LOCATION:P.2NO9.06 (La Plaine)
SEQUENCE:0
DESCRIPTION:Title: Nash equilibrium in multi-player multi-outcome games
on finite graphs\n\nAbstract: I will present some result in turn-based g
ames played on finite graphs. Instead of considering specific games with
specific preferences\, I will prove more abstract\, characterisation-li
ke results: existence of Nash equilibrium with simple strategies\, under
some condition.
END:VEVENT
BEGIN:VEVENT
CREATED:20180123T094409Z
UID:40A5CACF-4208-4795-A8CD-5E254A6F7142
DTEND;TZID=Europe/Brussels:20180427T163000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Isabelle Mainz (ULG)
DTSTART;TZID=Europe/Brussels:20180427T160000
DTSTAMP:20180123T094442Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
END:VEVENT
BEGIN:VEVENT
CREATED:20180117T115228Z
UID:891B56EE-71A2-4220-A937-FFB6A5E664CB
DTEND;TZID=Europe/Brussels:20180330T163000
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Guillermo A. Perez (ULB): Graph-Based Reductions for Model
Checking and Learning MDPs
DTSTART;TZID=Europe/Brussels:20180330T160000
DTSTAMP:20180117T115328Z
SEQUENCE:0
DESCRIPTION:Omega-regular objectives in Markov decision processes (MDPs)
reduce to reachability: find a policy which maximizes the probability o
f reaching a target set of states. Given an MDP\, an initial distributio
n\, and a target set of states\, such a policy can be computed by most p
robabilistic model checking tools. If the MDP is only partially specifie
d\, i.e.\, some prob- abilities are unknown\, then model-learning techni
ques can be used to statistically approximate the probabilities and enab
le the computation of the desired policy. For fully specified MDPs\, red
ucing the size of the MDP translates into faster model checking\; for pa
rtially specified MDPs\, into faster learning. We provide reduction tech
niques that allow us to remove irrelevant transition probabilities: tran
sition probabilities (known\, or to be learned) that do not influence th
e maximal reachability probability. Among other applications\, these red
uctions can be seen as a pre-processing of MDPs before model checking or
as a way to reduce the number of experiments required to obtain a good
approximation of an unknown MDP.
END:VEVENT
BEGIN:VEVENT
CREATED:20180122T112752Z
UID:ECB1C75B-32F2-4414-BC29-1429DDD2194D
DTEND;TZID=Europe/Brussels:20180330T121500
TRANSP:OPAQUE
X-APPLE-TRAVEL-ADVISORY-BEHAVIOR:AUTOMATIC
SUMMARY:[cfv] Thomas Brihaye (UMons): When are Stochastic Transition Sys
tems Tameable?
DTSTART;TZID=Europe/Brussels:20180330T114500
DTSTAMP:20180122T112752Z
LOCATION:ULB La Plaine NO\, Salle Solvay
SEQUENCE:0
DESCRIPTION:\nA decade ago\, Abdulla et al introduced the elegant concep
t of decisiveness for denumerable Markov chains. Roughly decisiveness al
lows one to lift most good properties from finite Markov chains to denum
erable ones\, and therefore to adapt existing verification algorithms to
infinite-state models. Denumerable Markov chains however do not encompa
ss stochastic real-time systems\, and general stochastic transition syst
ems (STSs) are needed. In this talk\, we discuss a framework to perform
both the qualitative and the quantitative analysis of STSs. In order to
do so\, we first need to adapt the concept of decisiveness for general S
TSs. Then we define a notion of abstraction and provide some transfer pr
operties. Then we focus on both qualitative and quantitative analysis. B
eyond (repeated) reachability properties for which our technics are stro
ngly inspired by the work on denumerable Markov chains\, we use abstract
ions to design algorithms for the model-checking of arbitrary omega-regu
lar properties\, for subclasses of STS. Last we instantiate our framewo
rk with stochastic timed automata Some of these results were known from
the literature\, but our generic approach permits to view them in a unif
ied framework. We also derive interesting new approximability results.\n
\nThis talk is based on joint work with Nathalie Bertrand\, Patricia Bou
yer\, and Pierre Carlier\n
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
END:STANDARD
END:VTIMEZONE
BEGIN:VTIMEZONE
TZID:Europe/Brussels
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
DTSTART:19810329T020000
TZNAME:GMT+2
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
DTSTART:19961027T030000
TZNAME:GMT+1
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VTIMEZONE
TZID:America/Chicago
BEGIN:DAYLIGHT
TZOFFSETFROM:-0600
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
DTSTART:20070311T020000
TZNAME:GMT-5
TZOFFSETTO:-0500
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0500
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
DTSTART:20071104T020000
TZNAME:GMT-6
TZOFFSETTO:-0600
END:STANDARD
END:VTIMEZONE
BEGIN:VTIMEZONE
TZID:/freeassociation.sourceforge.net/Tzfile/Europe/Brussels
X-LIC-LOCATION:Europe/Brussels
BEGIN:STANDARD
TZNAME:CET
DTSTART:19461007T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0100
END:STANDARD
BEGIN:STANDARD
TZNAME:CET
DTSTART:19770101T000000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19770403T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19770925T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19780402T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19781001T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19790401T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19790930T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19800406T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19800928T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19810329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19810927T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19820328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19820926T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19830327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19830925T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19840325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19840930T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19850331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19850929T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19860330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19860928T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19870329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19870927T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19880327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19880925T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19890326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19890924T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19900325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19900930T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19910331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19910929T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19920329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19920927T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19930328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19930926T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19940327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19940925T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19950326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19950924T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19960331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19961027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19970330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19971026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19980329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19981025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:19990328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:19991031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20000326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20001029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20010325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20011028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20020331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20021027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20030330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20031026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20040328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20041031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20050327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20051030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20060326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20061029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20070325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20071028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20080330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20081026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20090329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20091025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20100328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20101031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20110327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20111030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20120325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20121028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20130331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20131027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20140330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20141026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20150329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20151025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20160327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20161030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20170326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20171029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20180325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20181028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20190331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20191027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20200329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20201025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20210328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20211031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20220327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20221030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20250330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20251026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20260329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20261025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20270328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20271031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20280326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20281029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20290325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20291028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20300331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20301027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20310330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20311026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20320328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20321031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20330327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20331030T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20340326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20341029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20350325T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20351028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20360330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20361026T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20370329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
DTSTART:20371025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
END:VCALENDAR