text:
THE VISION THAT CAME TRUE
THE STAR CODE
MY VERY OWN STORY
Twisted Love
AMBER MASON
The Decline of Television
Bhubaneswar 20 ℃
TPH-Blog
Graffiti of Emotions
Scifi Thriller
Home/Categories/Psychological Thriller/HITCHHIKER
TPH February 9, 2020
"It's been a week. He hasn't even called me once," she thought while preparing the breakfast and pouring out some juice. She checked the calendar and the time. She was getting late for work.
"Need to work fast or I'll be late."
Dumping the dishes in the dishwasher, she rushed outside her house, making her way towards her car.
As soon as she reached her office in the hospital, she was bombarded with files and pending drafts that were piled on her desk. She groaned internally but still greeted her assistant with a beaming smile.
"Good Morning Martha."
"Good Morning, Ma'am," Martha replied while standing up from her seat and greeting her formally with an awkward smile and pushing a lock of hair behind her ears.
"How many times have I told you not to get so formal with me. Call me Nikki," she said with a wink and smile.
And the day passed by, and even before she knew, her department was empty. She huffed and looked at the clock which was already past seven. The sun had set. Lazily, she dragged herself off her seat and gathered her stuff, making way towards her car. She was checking her phone on the way for any new missed calls or messages, specifically from someone. But, nothing new popped on her phone. Heavy-heartedly, she stacked her bags inside the car and started the engine. She was halfway through to the destination when her phone rang. An unknown number blaring on her phone. Wrinkling her forehead, trying to jog her memory whether she knew that number from anywhere, she picked up her phone and hesitantly answered it.
"Hello Nikki," a deep baritone made her heart race a bit faster and she knew who the caller was. She had been waiting for this moment for almost a week now. Hurriedly she replied with a quick greeting and halted her car at a nearby parking space.
"How have you been, Nikki?"
"Well, the usual, work and other chores. What about you?"
She was getting sweaty, and her heart beat faster. She was getting nervous which made her say stupid things now and then. She would curse herself internally, whenever she would embarrass herself, and bite her lips occasionally. Old habits die hard. But today was different. Today she couldn't stop herself from biting her lips constantly. His words were replaced with static noise and as she sat in the driver's seat, still numb from the conversation she had and the information she got from her friend – that's what she thought until now though.
Reflecting on his words, the incidents of that night came barging in her mind. That night was darker than usual. There was no moon in the sky and the wind was blowing lightly. Nikki was on her way back home from work and it was later than usual. While on her way home, she had to take a long turn as there were some potholes on her usual route, which apparently was blocked. The other route was eerily empty and was a long stretch of nothingness. She turned her radio at a moderate volume to kill the weird emptiness of the way. In a distance, she could see a figure of someone walking along the side of the road. She could make out the big backpack he was carrying in her car's headlight. Getting a bit closer, she realized that the man had also noticed her presence as he stopped in his tracks and started waving his hand with a thumb struck out in a traditional hitchhiker way. Nikki got in an indecisive state as whether to stop and help this guy or to drive straight and never look back. But her kind and considerate counterpart wouldn't let her drive away. So, she slowed down her car, halted in front of the man and rolled down her window. She asked the man where was he heading and on knowing that the city was on her way home, she allowed him to get into the car. While in the car, she at once started a conversation to kill the silence.
He replied after thinking for a while looking straight ahead.
"My name's Neil and what would be yours by the way?"
At that, he turned his head towards her and smiled. He was a good-looking fellow with lots of freckles on his nose and a small dimple on his right cheek, that appeared only when he smiled. His chestnut brown hair was ruffled in a wavy mess and his dark eyes looked sleep-deprived. The ride, after his sweet dimpled smile, was smooth and filled with lots of small talks. Nikki was feeling more comfortable and even a bit closer to her newly found hitchhiker. After getting to the city, Nikki offered Neil to have dinner with her. He agreed. They went to a nearby restaurant and chatted happily over dinner. Nikki was overwhelmed as these occasions in her life were rare. Neil got all flustered when the time for paying the bill came. Nikki knew a little about his present financial condition, so she convinced him to let her pay for the food and let him buy the next time they meet. After dinner, they were back on the road and talked comfortably with each other. After reaching the destination, she turned off the engine and said goodbye. Neil saved her number to catch up with her later. Then, with a beaming smile on her face, she made her way home and slept with a warm feeling in her heart that night.
But the call today changed everything. Her feelings for him that were starting to grow, lay slaughtered. Over the phone, he said, "Nikki, I have to tell you something. Listen to me very carefully. Never allow a hitch-hiker in your car ever from now onwards. Because you don't know how dangerous it will be. I'm calling you to tell you that, that day I didn't get into your car for a ride but to high-jack your car, rape you and then kill you on the way and dump you in some nearby forest, and then steal your car and cash." All but silence is what followed his words. Thereby, he continued. "I couldn't do it though, after talking with you so much and getting to know you. And your smile was so warm, I couldn't help myself but feel guilty about what I was going to do. And then you offered me dinner. So, I decided against it and left that idea altogether. You are the kindest and warmest person I have ever known. So please, never let a hitchhiker in your car at odd times and especially at odd places." And that's when the line cut off and all that remained was the hum of static on the phone and her loud and heavy breathing.
Written by:- Muskan Priya
Facebook Twitter LinkedIn Tumblr Pinterest Reddit WhatsApp Telegram
Ding Dong!
Nine Floors Up
Immortal Love
ITS TIME TO BREAK-UP BIG TECH
Haliospume
"https://kinokraad.com" - kinokraad.com смотреть фильм онлай...
Donaldatope
Elbaszott egyenlettel kezdte Orbán szerint a Fidesz generáci...
tahas
Заказать seo поисковую оптимизацию сайта, Заказать услуги по...
ulikoh
Recent Airticles
Chandaka Industrial Estate Patia,
Bhubaneshwar, Odisha 751024
Email: contact@tph.org.in
URL: https://www.tph.org.in/
KIIT University 2017-18.
Share on Whatsapp Share
Share on Sms Share
© Copyright 2021, All Rights Reserved | TPH-Blog
Hey Buddy!, I found this information for you: "HITCHHIKER". Here is the website link: https://blog.tph.org.in/hitchhiker/. Thank you.
Privacy Center Cookie Policy


text:
The Men's Freestyle 65 kg competition of the wrestling events at the 2022 Mediterranean Games in Oran, Algeria, was held 27–28 June 2022 at the EMEC Hall.

Results
 Legend
 F — Won by fall

References

Men's Freestyle 65 kg

redpajama_set_name: RedPajamaWikipedia


The Paris Area Chamber of Commerce & Tourism issued the following announcement on March 1.
Today is the last day to submit nominations for the Parisian of the Year and Business of they Year Awards. We have so many deserving individuals and businesses in this town so get your nominations in!


text:
\section{Introduction}

In approaches to non-interleaving concurrency, more than one event may
happen concurrently.  There is a plethora of formalisms for modeling
and analyzing such concurrent systems, \eg~Petri
nets~\citep{book/Petri62}, event
structures~\citep{DBLP:journals/tcs/NielsenPW81}, configuration
structures~\citep{DBLP:conf/lics/GlabbeekP95,
  DBLP:journals/tcs/GlabbeekP09},
or more recent variations such as dynamic event
structures~\citep{DBLP:conf/forte/ArbachKPN15} and Unravel
nets~\citep{conf/acmsac/CasuP17}.  They all share the convention of
differentiating between concurrent and interleaving executions; using
CCS notation~\citep{book/Milner89}, $a| b\ne a. b+ b. a$.

For modeling and analyzing embedded or cyber-physical systems,
formalisms which use real time are available.  These include timed
automata~\citep{DBLP:journals/tcs/AlurD94}, time Petri
nets~\citep{journal/transcom/MerlinF76}, timed-arc Petri
nets~\citep{DBLP:conf/apn/Hanisch93}, or various classes of hybrid
automata~\citep{DBLP:journals/tcs/AlurCHHHNOSY95}.  Common for them all
is that they identify concurrent and interleaving executions; here,
$a| b= a. b+ b. a$.

We are interested in formalisms for real-time non-interleaving
concurrency.  Hence we would like to differentiate between concurrent
and interleaving executions and be able to model and analyze real-time
properties.  Few such formalisms seem to be available in the
literature.  (The situation is perhaps best epitomized by the fact
that there is a natural non-interleaving semantics for Petri
nets~\citep{DBLP:journals/iandc/GoltzR83} which is also used in
practice~\citep{DBLP:conf/spin/Esparza10,
  DBLP:series/eatcs/EsparzaH08}, but almost all work on real-time
extensions of Petri nets~\citep{journal/transcom/MerlinF76,
  DBLP:conf/apn/Hanisch93, DBLP:conf/performance/Sifakis77,
  DBLP:conf/formats/Srba08}, including the popular tool
TAPAAL\footnotemar
, use an interleaving semantics.

Also Uppaal\footnotemar
, the successful tool for modeling and analyzing networks of timed
automata, uses an interleaving semantics for such networks.  This
leads to great trouble with state-space explosion (see also
Sect.~\ref{se:tensor} of this paper) which, we believe, can be avoided
with a non-interleaving semantics such as we propose here.

We introduce higher-dimensional timed automata (HDTA), a formalism
based on the (non-interleaving) higher-dimensional automata
of~\citet{DBLP:journals/tcs/Glabbeek06, Glabbeek91-hda}
and~\citet{DBLP:conf/popl/Pratt91} and the timed automata
of~\citet{DBLP:journals/tcs/AlurD94, DBLP:conf/icalp/AlurD90}.  We
show that HDTA can model interesting phenomena which cannot be
captured by neither of the formalisms on which they are based, but
that their analysis remains just as accessible as the one of timed
automata.  That is, reachability for HDTA is PSPACE-complete and can
be decided using zone-based algorithms.

In the above-mentioned interleaving real-time formalisms, continuous
flows and discrete actions are orthogonal in the sense that executions
alternate between real-time delays and discrete actions which are
immediate, \ie~take no time.  (In the hybrid setting, these are
usually called flows and mode changes, respectively.)
Already~\citet{DBLP:conf/stacs/SifakisY96} notice that this
significantly simplifies the semantics of such systems and hints that
this is a main reason for the success of these formalisms (see the
more recent~\citet{DBLP:conf/formats/Srba08} for a similar
statement).%
\footnotetext{\url{http://www.tapaal.net/}}%
\footnotetext{\url{http://www.uppaal.org/}}

In the (untimed) non-interleaving setting, on the other hand, events
have a (logical, otherwise unspecified) duration.  This can be seen,
for example, in the ST-traces of~\citet{DBLP:journals/tcs/Glabbeek06}
where actions have a start ($a^+$) and a termination ($a^-$) and are
(implicitly) running between their start and termination, or in the
representation of concurrent systems as Chu spaces over
$3=\{ 0, \frac12, 1\}$, where $0$ is interpreted as ``before'',
$\smash[t]{\frac12}$ as ``during'', and $1$ as ``after'',
see~\citet{DBLP:journals/mscs/Pratt00}.  Intuitively, only if events
have duration can one make statements such as ``while $a$ is running,
$b$ starts, and then while $b$ is running, $a$ terminates''.

In our non-interleaving real-time setting, we hence abandon the
assumption that actions are immediate.  Instead, we take the view that
actions start and then run during some \emph{specific} time before
terminating.  While this runs counter to the standard assumption in
most of real-time and hybrid modeling, a similar view can be found,
for example, in~\citet{DBLP:conf/icalp/Cardelli82}.\footnote{The
  author wishes to thank Kim G.~Larsen for pointing him towards this
  paper.}

Given that we abandon the orthogonality between continuous flows and
discrete actions, we find it remarkable to see that the standard
techniques used for timed automata transfer to our non-interleaving
setting.  Equally remarkable is, perhaps, the fact that even though
\textit{``[t]he timed-automata model is at the very border of
  decidability, in the sense that even small additions to the
  formalism [\dots] will soon lead to the undecidability of
  reachability questions''}~\citep{book/AcetoILS07}, our extension to
higher dimensions and non-interleaving concurrency is completely free
of such trouble.

The contributions of this paper are, thus, (1)~the introduction of a
new formalism of HDTA, a natural extension of higher-dimensional
automata and timed automata, in Sect.~\ref{se:hdta}; (2)~the proof
that reachability for HDTA is PSPACE-complete and decidable using
zone-based algorithms, in Sects.~\ref{se:reach} and~\ref{se:zone};
(3)~the introduction of a tensor product for HDTA which can be used
for parallel composition, in Sect.~\ref{se:tensor}; and (4)~the
extension of the definition to higher-dimensional hybrid automata
together with a non-trivial example of two independently bouncing
balls, in Sect.~\ref{se:hybrid}.

\section{Preliminaries}
\label{se:hda}

We recall a few facts about higher-dimensional automata and timed
automata.

\subsection{Higher-Dimensional Automata}

Higher-dimensional automata are a generalization of finite automata
which permit the specification of independence of actions through
higher-dimensional elements.  That is, they consist of states and
transitions, but also squares which signify that two events are
independent, cubes which denote independence of three events, \etc.
To introduce them properly, we need to start with precubical sets.

A \emph{precubical set} is a graded set $X= \bigcup_{ n\in \Nat} X_n$,
with $X_n\cap X_m= \emptyset$ for $n\ne m$, together with mappings
$\delta_{ k, n}^\nu:X_n\to X_{ n- 1}$, $k= 1,\dots, n$, $\nu= 0, 1$,
satisfying the \emph{precubical identity}
\begin{equation*}
  \delta_{ k, n- 1}^\nu \delta_{ \ell, n}^\mu= \delta_{ \ell- 1, n- 1}^\mu
  \delta_{ k, n}^\nu \qquad( k< \ell)\,.
\end{equation*}

\begin{figure}[b]
  \centering
  \begin{tikzpicture}[>=stealth', x=1cm, y=.8cm]
    \tikzstyle{every node}=[font=\footnotesize]
    \tikzstyle{every state}=[fill=white,shape=circle,inner
    sep=.5mm,minimum size=3mm]
    \path[fill=black!15] (0,0) to (2,0) to (2,2) to (0,2) to (0,0);
    \node[state] (00) at (0,0) {};
    \node[state] (10) at (2,0) {};
    \node[state] (01) at (0,2) {};
    \node[state] (11) at (2,2) {};
    \path (00) edge (01);
    \path (00) edge (10);
    \path (01) edge (11);
    \path (10) edge (11);
    \node at (1,1) {$x$};
    \node at (-.4,1.05) {$\delta_1^0 x$};
    \node at (2.4,1.05) {$\delta_1^1 x$};
    \node at (1,-.25) {$\delta_2^0 x$};
    \node at (1,2.25) {$\delta_2^1 x$};
    \node at (-1,-.35) {$\delta_1^0 \delta_2^0 x= \delta_1^0
      \delta_1^0 x$};
    \node at (-1,2.35) {$\delta_1^0 \delta_2^1 x= \delta_1^1
      \delta_1^0 x$};
    \node at (3,-.35) {$\delta_1^1 \delta_2^0 x= \delta_1^0
      \delta_1^1 x$};
    \node at (3,2.35) {$\delta_1^1 \delta_2^1 x= \delta_1^1
      \delta_1^1 x$};
  \end{tikzpicture}
  \caption{%
    \label{fi:2cubefaces-full}
    A $2$-cube $x$ with its four faces $\delta_1^0 x$, $\delta_1^1 x$,
    $\delta_2^0 x$, $\delta_2^1 x$ and four corners}
\end{figure}

Elements of $X_n$ are called \emph{$n$-cubes}, and for $x\in X_n$,
$n= \dim x$ is its \emph{dimension}.  The mappings
$\delta_{ k, n}^\nu$ are called \emph{face maps}, and we will usually
omit the extra subscript $n$ and write $\delta_k^\nu$ instead of
$\delta_{ k, n}^\nu$.  Intuitively, each $n$-cube $x\in X_n$ has $n$
\emph{lower faces} $\smash[t]{\delta_1^0 x,\dotsc, \delta_n^0 x}$ and $n$
\emph{upper faces} $\delta_1^1 x,\dotsc, \delta_n^1 x$, and the
precubical identity expresses the fact that $( n- 1)$-faces of an
$n$-cube meet in common $( n- 2)$-faces; see
Fig.~\ref{fi:2cubefaces-full} for an example.

A precubical set $X$ is \emph{finite} if $X$ is finite as a set.  This
means that $X_n$ is finite for each $n\in \Nat$ and that $X$ is
\emph{finite-dimensional}: there exists $N\in \Nat$ such that
$X_n= \emptyset$ for all $n\ge N$.

Let $\Sigma$ be a finite set of \emph{actions} and recall that a
\emph{multiset} over $\Sigma$ is a mapping $\Sigma\to \Nat$.  We
denote multisets using double braces $\mlbrace\cdot\mrbrace$ and the
set of multisets over $\Sigma$ by $\Nat^\Sigma$.  The
\emph{cardinality} of $S\subseteq \Nat^\Sigma$ is
$| S|= \sum_{ a\in \Sigma} S( a)$.

A \emph{higher-dimensional automaton} (HDA) is a structure
$( X, x^0, X^f, \lambda)$, where $X$ is a finite precubical set with
initial state $x^0\in X_0$ and accepting states $X^f\subseteq X_0$,
and $\lambda: X\to \Nat^\Sigma$ is a labeling function such that for
every $x\in X$,
\begin{itemize}
\item $| \lambda( x)|= \dim x$,
\item $\lambda( \delta_k^0 x)= \lambda( \delta_k^1 x)$ for all
  $k\le n$, and
\item $\lambda( x)\setminus \lambda( \delta_k^0 x)$ is a singleton
  for all $k\le \dim x$.
\end{itemize}
The conditions on the labeling ensure that the label of an $n$-cube is
an extension, by one event, of the label of any of its faces.  The
computational intuition is that when passing from a lower face
$\delta_k^0 x$ of $x\in X$ to $x$ itself, the (unique) event in
$\lambda( x)\setminus \lambda( \delta_k^0 x)$ is started, and when
passing from $x$ to an upper face $\delta_\ell^1 x$, the event in
$\lambda( x)\setminus \lambda( \delta_\ell^1 x)$ is terminated.

\begin{figure}[t]
  \centering
  \begin{tikzpicture}[->,>=stealth',auto,x=1cm,y=1.3cm]

    \begin{scope}
      \path[fill=black!15] (0,0) to (2,0) to (2.7,.3) to (2.7,1.3) to
      (.7,1.3) to (0,1);
      \node[state, initial] (000) at (0,0) {};
      \node[state] (001) at (0,1) {};
      \node[state] (010) at (.7,.3) {};
      \node[state] (011) at (.7,1.3) {};
      \node[state] (100) at (2,0) {};
      \node[state] (101) at (2,1) {};
      \node[state] (110) at (2.7,.3) {};
      \node[state, accepting] (111) at (2.7,1.3) {};
      \path (000) edge node[below] {$a$} (100);
      \path (000) edge node[left] {$c$} (001);
      \path (000) edge (010);
      \path (001) edge (011);
      \path (001) edge (101);
      \path (010) edge (110);
      \path (010) edge (011);
      \path (100) edge node[below] {$b$} (110);
      \path (100) edge (101);
      \path (011) edge (111);
      \path (101) edge (111);
      \path (110) edge (111);
    \end{scope}
    \begin{scope}[xshift=15em]
      \path[fill=black!30] (0,0) to (2,0) to (2.7,.3) to (2.7,1.3) to
      (.7,1.3) to (0,1);
      \node[state, initial] (000) at (0,0) {};
      \node[state] (001) at (0,1) {};
      \node[state] (010) at (.7,.3) {};
      \node[state] (011) at (.7,1.3) {};
      \node[state] (100) at (2,0) {};
      \node[state] (101) at (2,1) {};
      \node[state] (110) at (2.7,.3) {};
      \node[state, accepting] (111) at (2.7,1.3) {};
      \path (000) edge node[below] {$a$} (100);
      \path (000) edge node[left] {$c$} (001);
      \path (000) edge (010);
      \path (001) edge (011);
      \path (001) edge (101);
      \path (010) edge (110);
      \path (010) edge (011);
      \path (100) edge node[below] {$b$} (110);
      \path (100) edge (101);
      \path (011) edge (111);
      \path (101) edge (111);
      \path (110) edge (111);
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:cube}
    Two example HDA.  Left, the hollow cube; right, the full cube}
\end{figure}

HDA can indeed model higher-order concurrency of actions.  As an
example, the hollow cube on the left of Fig.~\ref{fi:cube}, consisting
of all six faces of a cube but not of its interior, models the
situation where the actions $a$, $b$ and $c$ are mutually independent,
but cannot be executed all three concurrently.  The full cube on the
right of Fig.~\ref{fi:cube}, on the other hand, has $a$, $b$ and $c$
independent as a set.  The left HDA might model a system of three
users connected to two printers, so that every two of the users can
print concurrently but not all three, whereas the right HDA models a
system of three users connected to (at least) three printers.

\subsection{Timed Automata}

Timed automata extend finite automata with clock variables and
invariants which permit the modeling of real-time properties.
Let $C$ be a finite set of \emph{clocks}.  $\Phi( C)$ denotes the set
of \emph{clock constraints} defined as
\begin{multline*}
  \Phi( C)\ni \phi_1, \phi_2::= c\bowtie k\mid \phi_1\land
  \phi_2 \\
  ( c\in C, k\in \Int, \bowtie\in\{ \mathord<, \mathord\le,
  \mathord\ge, \mathord>\})\,.
\end{multline*}
Hence a clock constraint is a conjunction of comparisons of clocks to
integers.

A \emph{clock valuation} is a mapping $v: C\to \Realnn$, where
$\Realnn$ denotes the set of non-negative real numbers.  The
\emph{initial} clock valuation is $v^0: C\to \Realnn$ given by
$v^0( c)= 0$ for all $c\in C$.  For $v\in \Realnn^C$, $d\in \Realnn$,
and $C'\subseteq C$, the clock valuations $v+ d$ and $v[ C'\gets 0]$
are defined by
\begin{equation*}
  ( v+ d)( c)= v( c)+ d\,; \quad v[ C'\gets 0]( c)=
  \begin{cases}
    0 &\text{if } c\in C'\,, \\
    v( c) &\text{if } c\notin C'\,.
  \end{cases}
\end{equation*}
For $v\in \Realnn^C$ and $\phi\in \Phi( C)$, we write $v\models \phi$
if $v$ satisfies $\phi$ and
$\sem \phi=\{ v: C\to \Realnn\mid v\models \phi\}$.

A \emph{timed automaton} is a structure $( Q, q^0, Q^f, I, E)$, where
$Q$ is a finite set of locations with initial location $q^0\in Q$ and
accepting locations $Q^f\subseteq Q$, $I: Q\to \Phi( C)$ assigns
invariants to states, and
$E\subseteq Q\times \Phi( C)\times \Sigma\times 2^C\times Q$ is a set
of guarded transitions.

The \emph{semantics} of a timed automaton $A=( Q, q^0, Q^f, I, E)$ is
a (usually infinite) transition system
$\sem A=( S, s^0, S^f, \mathord\leadsto)$, with
$\mathord\leadsto\subseteq S\times S$, given as follows:
\begin{align*}
  S &=\{( q, v)\subseteq Q\times \Realnn^C\mid v\models I( q)\} \\
  s^0 &= ( l^0, v^0) \quad S^f= S\,\cap\, Q^f\!\!\times\! \Realnn^C \\
  \mathord\leadsto &= \{(( q, v),( q, v+ d))\mid \forall 0\le d'\le d:
  v+ d'\models I( q)\} \\
  &\quad \cup\{(( q, v),( q', v'))\mid \exists( q, \phi, a, C', q')\in
  E: \\
  &\hspace{12.5em} v\models \phi, v'= v[ C'\gets 0]\}
\end{align*}
Note that we are ignoring the labels here, as we will be concerned
with reachability only.  As usual, we say that $A$ is \emph{reachable}
iff there exists a finite path $s^0\leadsto\dotsm\leadsto s$ in $\sem
A$ for which $s\in S^f$.

The definition of $\leadsto$ ensures that actions are immediate:
whenever $( q, \phi, a, C', q')\in E$, then $A$ passes from $( q, v)$
to $( q', v')$ without any delay.  Time progresses only during delays
$( q, v)\leadsto( q, v+ d)$ in locations.

\section{Higher-Dimensional Timed Automata}
\label{se:hdta}

Unlike timed automata, higher-dimensional automata make no formal
distinction between states ($0$-cubes), transitions ($1$-cubes), and
higher-dimensional cubes.  We transfer this intuition to
higher-dimensional timed automata, so that each $n$-cube has an
invariant which specifies when it is enabled and an exit condition
giving the clocks to be reset when leaving:

\begin{defn}
  A \emph{higher-dimensional timed automaton} (HDTA) is a structure
  $( L, l^0, L^f, \lambda, \inv, \exit)$, where
  $( L, l^0, L^f, \lambda)$ is a finite higher-dimensional automaton
  and $\inv: L\to \Phi( C)$, $\exit: L\to 2^C$ assign \emph{invariant}
  and \emph{exit} conditions to each $n$-cube.
\end{defn}

The \emph{semantics} of a HDTA
$A=( L, l^0, L^f, \lambda, \inv, \exit)$ is a (usually infinite)
transition system $\sem A=( S, s^0, S^f, \mathord\leadsto)$, with
$\mathord\leadsto\subseteq S\times S$, given as follows:
\begin{align*}
  S &=\{( l, v)\subseteq L\times \Realnn^C\mid v\models \inv( l)\} \\
  s^0 &= ( l^0, v^0) \quad S^f= S\,\cap\, L^f\!\!\times\! \Realnn^C \\
  \mathord\leadsto &= \{(( l, v),( l, v+ d))\mid \forall 0\le d'\le d:
  v+ d'\models \inv( l)\} \\
  &\quad \cup\{(( \delta_k^0 l, v),( l, v'))\mid k\in\{ 1,\dotsc, \dim
  l\},  \\
  &\hspace{10em} v'= v[ \exit( \delta_k^0 l)\gets 0]\models \inv( l)\}
  \\
  &\quad \cup\{(( l, v),( \delta_k^1 l, v'))\mid k\in\{ 1,\dotsc, \dim
  l\}, \\
  &\hspace{10em} v'= v[ \exit( l)\gets 0]\models \inv( \delta_k^1 l)\}
\end{align*}
We omit labels from the semantics, as we will be
concerned only with \emph{reachability}:
Given a HDTA $A$, does there exist a finite path
$s^0\leadsto\dotsm\leadsto s$ in $\sem A$ such that $s\in S^f$?

Note that in the definition of $\leadsto$ above, we allow time to
evolve in any $n$-cube in $L$.  Hence transitions (\ie~$1$-cubes) are
not immediate.  The second line in the definition of $\leadsto$
defines the passing from an $( n-1)$-cube to an $n$-cube, \ie~the
start of a new concurrent event, and the third line describes what
happens when finishing a concurrent event.  Exit conditions specify
which clocks to reset when leaving a cube.

\begin{figure}[t]
  \centering
  \begin{tikzpicture}[>=stealth', x=1.3cm, y=.7cm]
    \begin{scope}
      \path[fill=black!15] (0,0) -- (4,0) -- (4,4) -- (0,4);
      \node[state, initial left] (00) at (0,0) {$l^0$};
      \node[state] (10) at (4,0) {$l_1$};
      \node[state] (01) at (0,4) {$l_2$};
      \node[state, accepting] (11) at (4,4) {$l^f$};
      \node[below] at (00.south) {$x, y\gets 0$};
      \node[below] at (10.south) {$x\ge 2; y\gets 0$};
      \node[above] at (01.north) {$y\ge 1; x\gets 0$};
      \node[above] at (11.north) {$x\ge 2\land y\ge 1$};
      \path (00) edge node[above] {$x\le 4; y\gets 0$} node[below]
      {$e_1 \qquad a$} (10);
      \path (00) edge node[left, align=right] {$y\le 3$ \\ $x\gets 0$
        \\ $e_2$} node[right] {$b$} (01);
      \path (10) edge node[right, align=left] {$x\ge 2$ \\$y\le 3$ \\
        $e_3$} node[left] {$b$} (11);
      \path (01) edge node[above] {$x\le 4\land y\ge 1$} node[below]
      {$e_4 \qquad a$} (11);
      \node[align=center] at (2,2) {$x\le 4\land y\le 3$ \\ $ab$};
      \node at (1,1) {$u$};
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:thda-ex1}
    The HDTA of Example~\ref{ex:thds-ex1}}
\end{figure}

\begin{exmp}
  \label{ex:thds-ex1}
  We give a few examples of two-dimensional timed automata.  The
  first, in Fig.~\ref{fi:thda-ex1}, models two actions, $a$ and $b$,
  which can be performed concurrently.  It consists of four states
  ($0$-cubes) $l^0, l_1, l_2, l^f$, four transitions ($1$-cubes) $e_1$
  through $e_4$, and one $ab$-labeled square ($2$-cube)~$u$.

  This HDTA models that performing $a$ takes between two and four time
  units, whereas performing $b$ takes between one and three time
  units.  To this end, we use two clocks $x$ and $y$ which are reset
  when the respective actions are started and then keep track of how
  long they are running.

  Hence $\exit( l^0)=\{ x, y\}$, and the invariants $x\le 4$ at the
  $a$-labeled transitions $e_1$, $e_4$ and at the square $u$ ensure
  that $a$ takes at most four time units.  The invariants $x\ge 2$ at
  $l_1$, $e_3$ and $l^f$ take care that $a$ cannot finish before two
  time units have passed.  Note that $x$ is also reset when exiting
  $e_2$ and $l_2$, ensuring that regardless when $a$ is started,
  whether before $b$, while $b$ is running, or after $b$ is
  terminated, it must take between two and four time units.
\end{exmp}

\begin{figure}[b]
  \centering
  \begin{tikzpicture}[>=stealth', x=1.3cm, y=.6cm]
    \begin{scope}[yshift=-5cm]
      \path[fill=black!15] (0,0) -- (4,0) -- (4,4) -- (0,4);
      \node[state, initial left] (00) at (0,0) {};
      \node[state] (10) at (4,0) {};
      \node[state] (01) at (0,4) {};
      \node[state, accepting] (11) at (4,4) {};
      \node[below] at (00.south) {$x, y\gets 0$};
      \node[below] at (10.south) {$x\ge 2; y\gets 0$};
      \node[above] at (01.north) {$y\ge 1; x\gets 0$};
      \node[above] at (11.north) {$x\ge 2\land y\ge 1$};
      \path (00) edge node[above] {$x\le 4; y\gets 0$} node[below]
      {$a$} (10);
      \path (00) edge node[left, align=right] {$y\le 3$ \\
        $\textcolor{red}{x\ge 1}$ \\ $x\gets 0$} node[right] {$b$}
      (01);
      \path (10) edge node[right, align=left] {$x\ge 2$ \\ $y\le 3$}
      node[left] {$b$} (11);
      \path (01) edge node[above] {$x\le \textcolor{red}{5}\land y\ge
        1$} node[below]
      {$a$} (11);
      \node[align=center] at (2,2) {$\textcolor{red}{1\le{}} x\le
        4\land y\le 3$ \\ $ab$};
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:thda-ex2}
    The HDTA of Example~\ref{ex:thda-ex2}}
\end{figure}

\begin{exmp}
  \label{ex:thda-ex2}
  In the HDTA shown in Fig.~\ref{fi:thda-ex2} (where we have omitted
  the names of states etc.\ for clarity and show changes to
  Fig.~\ref{fi:thda-ex1} in \textcolor{red}{red}), invariants have
  been modified so that $b$ can only start after $a$ has been running
  for one time unit, and if $b$ finishes before $a$, then $a$ may run
  one time unit longer.  Hence an invariant $x\ge 1$ is added to the
  two $b$-labeled transitions and to the $ab$-square (at the
  right-most $b$-transition $x\ge 1$ is already implied), and the
  condition on $x$ at the top $a$-transition is changed to $x\le 5$.

  Note that the left edge is now permanently disabled: before entering
  it, $x$ is reset to zero, but its edge invariant is $x\ge 1$.  This
  is as expected, as $b$ should not be able to start before~$a$.
\end{exmp}

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[>=stealth', x=1.3cm, y=.6cm]
    \begin{scope}[yshift=-10cm]
      \path[fill=black!15] (0,0) -- (4,0) -- (4,4) -- (0,4);
      \node[state, initial left] (00) at (0,0) {};
      \node[state] (10) at (4,0) {};
      \node[state] (01) at (0,4) {};
      \node[state, accepting] (11) at (4,4) {};
      \node[below] at (00.south) {$x, y\gets 0$};
      \node[below] at (10.south) {$x\ge 2\land \textcolor{red}{z\ge 1};
        y\gets 0$};
      \node[above] at (01.north) {$y\ge 1; x\gets 0$};
      \node[above] at (11.north) {$x\ge 2\land y\ge 1\land
        \textcolor{red}{z\ge 1}$};
      \path (00) edge node[above] {$x\le 4; y\gets 0$} node[below]
      {$a$} (10);
      \path (00) edge node[left, align=right] {$x\ge 1$ \\ $y\le
        3$ \\ $x, \textcolor{red}{z}\gets 0$} node[right]
      {$b$} (01);
      \path (10) edge node[right, align=left] {$x\ge 2$ \\ $y\le 3$ \\
        $\textcolor{red}{z\ge 1}$ \\ $\textcolor{red}{z\gets 0}$}
      node[left] {$b$} (11);
      \path (01) edge node[above, pos=.45] {$x\le 5\land y\ge
        1$} node[below]
      {$a$} (11);
      \node[align=center] at (2,2) {$1\le x\le 4\land y\le 3$ \\
        $\textcolor{red}{z\gets 0};\; ab$};
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:thda-ex3}
    The HDTA of Example~\ref{ex:thda-ex3}}
\end{figure}

\begin{exmp}
  \label{ex:thda-ex3}
  The HDTA in Fig.~\ref{fi:thda-ex3} (where we show changes to
  Fig.~\ref{fi:thda-ex2} in \textcolor{red}{red}) models the
  additional constraint that $b$ also \emph{finish} one time unit
  before $a$.  To this end, an extra clock $z$ is introduced which is
  reset when $b$ terminates and must be at least $1$ when $a$ is
  terminating.  After these changes, the right $b$-labeled edge is
  deadlocked: when leaving it, $z$ is reset to zero but needs to be at
  least one when entering the accepting state.  Again, this is
  expected, as $a$ should not terminate before~$b$.

  As both vertical edges are now permanently disabled, the accepting
  state can only be reached through the square.  This shows that
  reachability for HDTA cannot be reduced to one-dimensional
  reachability along transitions and relates them to the partial HDA
  of~\citet{DBLP:conf/calco/FahrenbergL15}.
\end{exmp}

\section{One-Dimensional Timed Automata}

We work out the relation between one-dimensional HDTA (\ie~1DTA) and
standard timed automata.  Note that this is not trivial, as in timed
automata, clocks can only be reset at transitions, and, semantically,
transitions take no time.  In contrast, in our 1DTA, resets can occur
in states and transitions may take time.

\begin{prop}
  There is a linear-time algorithm which, given any timed
  automaton $A$, constructs a 1DTA $A'$, with one extra clock, so that
  $A$ is reachable iff $A'$ is.
\end{prop}

\begin{pf}
  Let $A=( Q, q^0, Q^f, I, E)$ be a timed automaton.  It is clear that
  $L= Q\cup E$ forms a one-dimensional precubical set, with $L_0= Q$,
  $L_1= E$, $\delta_1^0( q, \phi, a, C', q')= q$, and
  $\delta_1^1( q, \phi, a, C', q')= q'$.  Let $l^0= q^0$ and
  $L^f= Q^f$.  In order to make transitions immediate, we introduce a
  fresh clock $c\notin C$.

  For $q\in Q$, let $\lambda( q)= \emptyset$, $\inv( q)= I( q)$, and
  $\exit( q)=\{ c\}$.  For $e=( q, \phi, a, C', q')\in E$, put
  $\lambda( e)=\{ a\}$, $\inv( e)= \phi\land( c\le 0)$, and
  $\exit( e)= C'$.  We have defined a 1DTA
  $A'=( L, l^0, L^f, \lambda, \inv, \exit)$ (over clocks
  $ C\cup\{ c\}$).
  %
  As $c$ is reset whenever exiting a state, and every transition has
  $c\le 0$ as part of its invariant, it is clear that transitions in
  $A'$ take no time, and the claim follows.
\qed\end{pf}

\begin{prop}
  There is a linear-time algorithm which, given any 1DTA $A$,
  constructs a timed automaton $A'$ over the same clocks such that $A$
  is reachable iff $A'$ is.
\end{prop}

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[>=stealth']
    \begin{scope}
      \node[state] (0) at (0,0) {};
      \node[state] (2) at (4,0) {};
      \node at (0,.3) {$\phi_1, C_1$};
      \node at (4,.3) {$\phi_3, C_3$};
      \path (0) edge node[above] {$\phi_2, C_2$} node[below] {$a$}
      (2);
    \end{scope}
    \path (2,-.5) edge[double] (2,-1.2);
    \begin{scope}[yshift=-1.9cm]
      \node[state] (0) at (0,0) {};
      \node[state] (1) at (2,0) {};
      \node[state] (2) at (4,0) {};
      \node at (0,.3) {$\phi_1$};
      \node at (2,.3) {$\phi_2$};
      \node at (4,.3) {$\phi_3$};
      \path (0) edge node[above] {$\ltrue, C_1$} (1);
      \path (1) edge node[above] {$\ltrue, C_2$} node[below] {$a$}
      (2);
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:ta-to-t1da}
    Conversion of 1DTA edge to timed automaton}
\end{figure}

\begin{pf}
  Let $A=( L, l^0, L^f, \lambda, \inv, \exit)$ be a 1DTA, we construct
  a timed automaton $A'=( Q, q^0, Q^f, I, E)$.  Because transitions in
  $A$ may take time, we cannot simply let $Q= L_0$, but need to add
  extra states corresponding to the edges in $L_1$.  Let, thus,
  $Q= L$, $I= \inv$, and
  $E=\{( \delta_1^0 x, \ltrue, \tau, \exit( \delta_1^0 x), x) ,( x,
  \ltrue, \lambda( x), \exit( x), \delta_1^1 x)\mid x\in L_1\}$,
  where $\tau\notin \Sigma$ is a fresh (silent) action.  See
  Fig.~\ref{fi:ta-to-t1da}.
\qed\end{pf}

Note that even though silent transitions in timed automata are a
delicate matter~\citep{DBLP:journals/fuin/BerardPDG98}, the fact that
we add them in the last proof is unimportant as we are only concerned
with reachability.  PSPACE-completeness of reachability for timed
automata now implies the following:

\begin{cor}
  \label{co:PSPACE}
  Reachability for HDTA is PSPACE-hard.
\end{cor}

\section{Reachability for HDTA is in PSPACE}
\label{se:reach}

We now turn to extend the notion of \emph{regions} to HDTA, in order
to show that reachability for HDTA is decidable in PSPACE.

\begin{defn}
  Let $( L, l^0, L^f, \lambda, \inv, \exit)$ be a HDTA and
  $R\subseteq L\times \Realnn^C\times L\times \Realnn^C$.  Then $R$ is
  an \emph{untimed bisimulation} if
  $(( l^0, v^0),( l^0, v^0))\in R$ and, for all
  $(( l_1, v_1),( l_2, v_2))\in R$,
  \begin{compactitem}
  \item $l_1\in L^f$ iff $l_2\in L^f$;
  \item whenever $( l_1, v_1)\leadsto( l_1', v_1')$, then also $( l_2,
    v_2)\leadsto( l_2', v_2')$ for some $(( l_1', v_1'),( l_2',
    v_2'))\in R$;
  \item whenever $( l_2, v_2)\leadsto( l_2', v_2')$, then also $( l_1,
    v_1)\leadsto( l_1', v_1')$ for some $(( l_1', v_1'),( l_2',
    v_2'))\in R$.
  \end{compactitem}
\end{defn}

For a HDTA $A$, let $\cmax A$ denote the maximal constant appearing in
any $\inv( l)$ for $l\in L$, and let $\req$ denote standard region
equivalence~\citep{DBLP:journals/tcs/AlurD94}.  Extend $\req$ to
$\sem A$ by defining $( l, v)\req( l', v')$ iff $l= l'$ and
$v\req v'$.

\begin{lem}
  $\req$ is an untimed bisimulation.
\end{lem}

\begin{pf}
  This follows from standard properties of region
  equivalence~\citep{DBLP:journals/tcs/AlurD94}.
\qed\end{pf}

For any HDTA $A$, the \emph{quotient} of
$\sem A=( S, s^0, S^f, \mathord\leadsto)$ under an untimed
bisimulation $R$ is defined, as usual, as
$\sem A/ R=( S/ R,[ s^0]_R, S^f/ R, \mathord{ \tilde\leadsto})$, where
$S/ R$ is the set of equivalence classes, $[ s^0]_R$ is the
equivalence class in which $s^0$ belongs, and
$\mathord{ \tilde\leadsto}\subseteq S/ R\times S/ R$ is defined by
$\tilde s\mathrel{ \tilde\leadsto} \tilde s'$ iff $\exists s\in \tilde
s, s'\in \tilde s': s\leadsto s'$.

\begin{lem}
  Let $A$ be a HDTA and $R$ an untimed bisimulation on $A$.
  Then $A$ is reachable iff $\sem A/ R$ is.
\end{lem}

\begin{pf}
  By definition, an accepting location is reachable in $A$ iff an
  accepting state is reachable in $\sem A$.  On $\sem A$, $R$ is a
  standard bisimulation, hence the claim follows.
\qed\end{pf}

\begin{lem}
  For any HDTA $A$, the quotient $\sem A/ \mathord{ \req}$ is finite.
\end{lem}

\begin{pf}
  This follows immediately from the standard fact that the set of
  clock regions, \ie~$\Realnn^C/ \mathord{ \req}$, is
  finite~\citep{DBLP:journals/tcs/AlurD94}.
\qed\end{pf}

The size of $\sem A/ \mathord{ \req}$ is exponential in the size of
$A$, but reachability in $\sem A/ \mathord{ \req}$ can be decided in
PSPACE, see~\citep{DBLP:journals/tcs/AlurD94}.  Together with
Corollary~\ref{co:PSPACE}, we conclude:

\begin{thm}
  Reachability for HDTA is PSPACE-complete.
\end{thm}

\section{Zone-Based Reachability}
\label{se:zone}

We show that the standard zone-based algorithm for checking
reachability in timed automata also applies in our HDTA setting.  This
is important, as zone-based reachability checking is at the basis of
the success of tools such as Uppaal,
see~\citep{DBLP:journals/sttt/LarsenPY97}.

Recall that the set $\Phi^+(C)$ of \emph{extended clock constraints}
over $C$ is defined by the grammar
\begin{multline*}
  \Phi^+( C)\ni \phi_1, \phi_2::= c\bowtie k\mid c_1- c_2\bowtie
  k\mid \phi_1\land \phi_2 \\
  ( c, c_1, c_2\in C, k\in \Int, \bowtie\in\{ \mathord<, \mathord\le,
  \mathord\ge, \mathord>\}),
\end{multline*}
and that a \emph{zone} over $C$ is a subset $Z\subseteq \Realnn^C$
which can be represented by an extended clock constraint $\phi$,
\ie~such that $Z= \sem \phi$.  Let $\mcal Z( C)$ denote the set of
zones over $C$.

For a zone $Z\in \mcal Z( C)$ and $C'\subseteq C$, the \emph{delay}
and \emph{reset} of $Z$ are given by $Z^\uparrow=\{ v+ d\mid v\in Z\}$
and $Z[ C'\gets 0]=\{ v[ C'\gets 0]\mid v\in Z\}$; these are again
zones, and their representation by an extended clock constraint can be
efficiently computed~\citep{DBLP:conf/ac/BengtssonY03}.  Also zone
inclusion $Z'\subseteq Z$ can be efficiently decided.

The \emph{zone graph} of a HDTA
$A=( L, l^0, L^f, \lambda, \inv, \exit)$ is a (usually infinite)
transition system $Z( A)=( S, s^0, S^f, \mathord\leadsto)$, with
$\mathord\leadsto\subseteq S\times S$, given as follows:
\begin{align*}
  S &=\{( l, Z)\subseteq L\times \mcal Z( C)\mid Z\subseteq \sem{
    \inv( l)}\} \\
  s^0 &= ( l^0, \sem{ v^0}^\uparrow\cap\sem{ \inv( l^0)}) \qquad S^f=
  S\,\cap\, L^f\!\!\times\! \mcal Z( C) \\
  \mathord\leadsto &= \{(( \delta_k^0 l, Z),( l, Z'))\mid k\in\{
  1,\dotsc, \dim l\}, \\
  &\hspace{9.5em} Z'= Z[ \exit( \delta_k^0 l)\gets 0]^\uparrow\cap
  \sem{ \inv( l)}\} \\
  &\;\cup\{(( l, Z),( \delta_k^1 l, Z'))\mid k\in\{ 1,\dotsc, \dim
  l\}, \\
  &\hspace{9.5em} Z'= Z[ \exit( l)\gets 0]^\uparrow\cap \sem{ \inv(
    \delta_k^1 l)}\}
\end{align*}

\begin{lem}
  For any HDTA $A$, an accepting location is reachable in $A$ iff an
  accepting state is reachable in $Z( A)$.
\end{lem}

\begin{pf}
  This follows from standard arguments as to the soundness and
  completeness of the zone abstraction~\citep{DBLP:journals/tcs/AlurD94}.
\qed\end{pf}

Any standard \emph{normalization}
technique~\citep{DBLP:conf/ac/BengtssonY03} may now be used to ensure
that the zone graph $Z( A)$ is finite, and then the standard zone
algorithms can be employed to efficiently decide reachability in HDTA.
As an example, Fig.~\ref{fi:zone} shows the zone graph of the HDTA in
Fig.~\ref{fi:thda-ex1} (Example~\ref{ex:thds-ex1}), with zones
displayed graphically using $x$ as the horizontal axis and $y$ as the
vertical.  (We have taken the liberty to simplify by computing unions
of zones at the locations $u$, $e_3$ and $e_4$ before proceeding.)

\begin{figure}[t]
  \centering
  \begin{tikzpicture}[>=stealth']
    \node[state with output, initial below] (l0) at (0,0)
    {$\vphantom{e_1}l^0$ \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw (0,0) -- (4.9,4.9);
      \end{tikzpicture}
    };
    \node[state with output] (e1) at (3,0) {$\vphantom{l^0}e_1$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw (0,0) -- (4,4);
      \end{tikzpicture}
    };
    \node[state with output] (l1) at (6.5,0) {$\vphantom{l^0}l_1$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (4.9,4.9) -- (2,2) -- (2,0) -- (4,0) --
        (4.9,.9);
      \end{tikzpicture}
    };
    \node[state with output] (u1) at (3.5,2.5) {$\vphantom{l^0_1}u$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (0,0) -- (4,0) -- (4,3) -- (3,3) -- (0,0);
      \end{tikzpicture}
    };
    \node[state with output] (e2) at (0,3) {$\vphantom{l^0}e_2$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw (0,0) -- (3,3);
      \end{tikzpicture}
    };
    \node[state with output] (l2) at (0,6) {$\vphantom{l^0}l_2$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (1.9,4.9) -- (0,3) -- (0,1) -- (1,1) --
        (4.9,4.9);
      \end{tikzpicture}
    };
    \node[state with output] (u2) at (2.5,3) {$\vphantom{l^0_1}u$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (0,0) -- (0,3) -- (3,3) -- (0,0);
      \end{tikzpicture}
    };
    \node[draw, rectangle] (u) at (3,2.75) {%
      \begin{tikzpicture}[scale=2.6,>=]
        \path (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0);
      \end{tikzpicture}
    };
    \node[state with output] (e41) at (2.5,6.5) {$\vphantom{l^0}e_4$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (3.9,4.9) -- (0,1) -- (0,4.9);
      \end{tikzpicture}
    };
    \node[state with output] (e42) at (3.5,6) {$\vphantom{l^0}e_4$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (0,1) -- (4,1) -- (4,3) -- (0,3) -- (0,1);
      \end{tikzpicture}
    };
    \node[draw, rectangle] (e4) at (3,6.25) {%
      \begin{tikzpicture}[scale=2.6,>=]
        \path (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0);
      \end{tikzpicture}
    };
    \node[state with output] (e31) at (7,2.5) {$\vphantom{l^0}e_3$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (4.9,0) -- (2,0) -- (4.9,2.9);
      \end{tikzpicture}
    };
    \node[state with output] (e32) at (6,3) {$\vphantom{l^0}e_3$
      \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \draw[fill=gray] (2,0) -- (4,0) -- (4,3) -- (2,3) -- (2,0);
      \end{tikzpicture}
    };
    \node[draw, rectangle] (e3) at (6.5,2.75) {%
      \begin{tikzpicture}[scale=2.6,>=]
        \path (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0);
      \end{tikzpicture}
    };
    \node[state with output] (lf1) at (7,6)
    {$\vphantom{e_1}l^f$ \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \path[fill=gray] (4.9,1) -- (2,1) -- (2,3) -- (3.9,4.9) --
        (4.9,4.9);
        \draw (4.9,1) -- (2,1) -- (2,3) -- (3.9,4.9);
      \end{tikzpicture}
    };
    \node[state with output] (lf2) at (6,6.5)
    {$\vphantom{e_1}l^f$ \nodepart{two}%
      \begin{tikzpicture}[scale=.2,>=]
        \draw[gray!40, very thin] (-.5,-.5) grid (4.9,4.9);
        \draw[gray!80, thin] (0,0) to (4.9,0);
        \draw[gray!80, thin] (0,0) to (0,4.9);
        \path[fill=gray] (4.9,1.9) -- (4,1) -- (2,1) -- (2,4.9) --
        (4.9,4.9);
        \draw (4.9,1.9) -- (4,1) -- (2,1) -- (2,4.9);
      \end{tikzpicture}
    };
    \path (l0) edge (e1);
    \path (e1) edge (l1);
    \path (e1) edge (u1);
    \path (l0) edge (e2);
    \path (e2) edge (l2);
    \path (e2) edge (u2);
    \path (l2) edge (e41);
    \path (u) edge (e42);
    \path (l1) edge (e31);
    \path (u) edge (e32);
    \path (e3) edge (lf1);
    \path (e4) edge (lf2);
  \end{tikzpicture}
  \caption{%
    \label{fi:zone}
    Zone graph of the HDTA in Fig.~\ref{fi:thda-ex1}}
\end{figure}

\section{Parallel Composition of HDTA}
\label{se:tensor}

There is a \emph{tensor product} on precubical sets which extends to
HDTA and can be used for parallel composition:

\begin{defn}
  Let $A_i=( L^i, l^{ i, 0}, L^{ i, f}, \lambda^i, \inv^i, \exit^i)$, for
  $i= 1, 2$, be HDTA.  The \emph{tensor product} of $A^1$ and $A^2$ is
  $A^1\otimes A^2=( L, l^0, L^f, \lambda, \inv, \exit)$ given as
  follows:
  \begin{gather*}
    L_n= \bigsqcup_{ p+ q= n} L^1_p\times L^2_q \quad\;\;
    l^0= ( l^{ 1, 0}, l^{ 2, 0}) \quad L^f= L^{ 1, f}\times L^{ 2,
      f} \\
    \delta_i^\nu( l^1, l^2)=
    \begin{cases}
      ( \delta_i^\nu l^1, l^2) &\!\!\!\!\text{if } i\le \dim l^1 \\
      ( l^1, \delta_{ i- \dim l^1}^\nu l^2) &\!\!\!\!\text{if } i>
      \dim l^1
    \end{cases} \\
    \lambda( l^1, l^2)= \lambda( l^1)\sqcup \lambda( l^2) \qquad
    \inv( l^1, l^2)= \inv( l^1)\land \inv( l^2) \\
    \exit( l^1, l^2)= \exit( l^1)\sqcup \exit( l^2)
  \end{gather*}
\end{defn}

Intuitively, tensor product is asynchronous parallel composition, or
independent product.  In combination with relabeling and restriction,
any parallel composition operator can be obtained,
see~\citet{WinskelN95-Models}
or~\citet{DBLP:conf/fossacs/Fahrenberg05} for the special case of HDA.

\begin{figure}[b]
  \centering
  \begin{tikzpicture}[>=stealth', x=.7cm, y=.3cm]
    \begin{scope}
      \node[state, initial below] (00) at (0,0) {};
      \node[state, accepting] (10) at (4,0) {};
      \node[state, initial below] (01) at (7,0) {};
      \node[state, accepting] (11) at (11,0) {};
      \node[above] at (00.north) {$x\gets 0$};
      \node[above] at (10.north) {$x\ge 2$};
      \node[above] at (01.north) {$y\gets 0$};
      \node[above] at (11.north) {$y\ge 1$};
      \path (00) edge node[above] {$x\le 4$} node[below] {$a$} (10);
      \path (01) edge node[above] {$y\le 3$} node[below] {$b$} (11);
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:tensor-ex}
    The two 1DTA of Example~\ref{ex:tensor-ex}}
\end{figure}

\begin{exmp}
  \label{ex:tensor-ex}
  Of the two 1DTA in Fig.~\ref{fi:tensor-ex}, the first models the
  constraint that performing the action $a$ takes between two and four
  time units, and the second, that performing $b$ takes between one
  and three time units.  (In the notation
  of~\citet{DBLP:conf/icalp/Cardelli82}, these are
  $a[2]\mathord: a(2)\mathord: 0$ and
  $b[1]\mathord: b(2)\mathord: 0$.)  Their tensor product is precisely
  the HDTA of Example~\ref{ex:thds-ex1}.
\end{exmp}

Using tensor product for parallel composition, one can avoid
introducing spurious interleavings and thus combat state-space
explosion.  Take the real-time version of Milner's scheduler
from~\citet{DBLP:journals/sttt/DavidLLNTW15} as an example.  This is
essentially a real-time round-robin scheduler in which the nodes are
simple timed automata, see Fig.~\ref{fi:milner} for the Uppaal model.

\begin{figure}[tbp]
  \centering

  \includegraphics*[width=.9\linewidth, bb=1.5cm 24cm 7cm 26.7cm]{milner-uppaal}
  \caption{%
    \label{fi:milner}
    Uppaal model of a single node in Milner's scheduler}
\end{figure}

Notice that there are, essentially, two transitions from the initial
to the topmost state, one which outputs w[i] (``work'') and another
which passes on the token (rec[(i+1)\%N]!).  These transitions are
independent, but because of the limitations of the timed-automata
formalism, they have to be modeled as an interleaving diamond.  Thus,
when a number of such nodes ($N = 30$, say) are composed into a
scheduler, a high amount of interleaving is generated: but most of it
is spurious, owing to constraints of the modeling language rather than
properties of the system at hand.

\citet{DBLP:journals/sttt/DavidLLNTW15}~show that especially when $d$
is much smaller than $D$ (say, $d = 4$ and $D = 30$), verification of
the scheduler becomes impossible already for $N = 6$ nodes.  The
authors then show that this can be amended by using compositional
verification techniques, which are out of scope of our current work.

Another possibility is to use methods from partial order
reduction~\citep{DBLP:books/sp/Godefroid96} to \emph{detect} spurious
interleavings.  Aside from the fact that this has proven to be largely
impractical for timed automata, see for
example~\citet{DBLP:conf/cav/HansenLLN014}, we also argue that by
using HDTA as a modeling language, partial order reduction is, so to
speak, \emph{built into} the model.  Spurious interleavings are taken
care of during the modeling phase, instead of having to be detected
during the verification phase.

A 2DTA corresponding to the Uppaal model in Fig.~\ref{fi:milner} is
essentially the tensor product of the w[i] and rec[(i+1)\%N]!
transitions, together with $1$-dimensional loops and a transition from
the upper to lower corner for the rec[i]? input transitions.

\section{Higher-Dimensional Hybrid Automata}
\label{se:hybrid}

For completeness, we show that our definition of HDTA easily extends
to one for higher-dimensional hybrid automata.  Let $X$ be a finite
set of variables, $\dot X=\{ \dot x\mid x\in X$,
$X'=\{ x'\mid x\in X\}$, and $\Pred( Y)$ the set of (arithmetic)
predicates on free variables in $Y$.

\begin{defn}
  A \emph{higher-dimensional hybrid automaton} (HDHA) is a structure
  $( L, \lambda, \inv, \flow, \exit)$, where $( L, \lambda)$ is a
  finite higher-dimensional automaton and
  $\init, \inv: L\to \Pred( X)$,
  $\smash[t]{\flow: L\to \Pred( X\cup \dot X)}$, and
  $\exit: L\to \Pred( X\cup X')$ assign \emph{initial},
  \emph{invariant}, \emph{flow}, and \emph{exit} conditions to each
  $n$-cube.
\end{defn}

Note that we have removed initial and final locations from the
definition; this is standard for hybrid automata.

The \emph{semantics} of a HDHA
$A=( L, \lambda, \inv, \flow, \exit)$ is a (usually
infinite) transition system $\sem A=( S, S^0, \mathord\leadsto)$,
with $\mathord\leadsto\subseteq S\times S$, given as follows:
\begin{align*}
  S &= \{( l, v)\subseteq L\times \Realnn^X\mid v\models \inv( l)\} \\
  S^0 &= \{( l, v)\in S\mid v\models \init(l)\} \\
  \mathord\leadsto &= \{(( l, v),( l, v'))\mid \exists d\ge 0, f\in
  \Diff([ 0, d], \Real^X): \\
  &\hspace{8.2em} f( 0)= v, f( d)= v', \forall t\in \mathopen]
  0, d\mathclose[: \\
  &\hspace{8.2em} f( t)\models \inv( q),( f( t), \dot f( t))\models
  \flow( q)\} \\
  &\quad \cup\{(( \delta_k^0 l, v),( l, v'))\mid k\in\{ 1,\dotsc, \dim
  l\},  \\[-.5ex]
  &\hspace{14em} ( v, v')\models \exit( \delta_k^0 l)\}
  \\
  &\quad \cup\{(( l, v),( \delta_k^1 l, v'))\mid k\in\{ 1,\dotsc, \dim
  l\}, \\[-.5ex]
  &\hspace{14em} ( v, v')\models \exit( l)\}
\end{align*}
Here $\Diff(D_1, D_2)$ denotes the set of differentiable functions
$D_1\to D_2$.

\begin{figure}[tbp]
  \centering
  \begin{tikzpicture}[>=stealth', x=1.3cm, y=.7cm]
    \begin{scope}
      \path[fill=black!15] (0,0) -- (4,0) -- (4,4) -- (0,4);
      \node[state] (00) at (0,0) {};
      \node[state] (10) at (4,0) {};
      \node[state] (01) at (0,4) {};
      \node[state] (11) at (4,4) {};
      \node[align=center] at (2,2) {%
        $\inv: x_1, x_2\ge 0$ \\
        $\flow: \dot x_1 = v_1, \dot v_1 = -g,
        $
        \\

        \dot x_2 = v_2, \dot v_2 = -g, \dot r = 0$ \\
        $\exit: r'= 0$
      };
      \path (10) edge node[right, align=left] {%
        $\inv: x_1 = 0, v_1\le 0,$ \\
        $x_2\ge 0, r\le \epsilon$ \\
        $\flow: \dot x_1 = 0, \dot v_1 = 0,$ \\
        $\dot x_2 = v_2, \dot v_2 = -g, \dot r = 1$ \\
        $\exit: r = \epsilon, r' = 0,$ \\
        $v_1' = -c v_1$
      } (11);
      \path (00) edge node[below, align=center] {%
        $\inv: x_2 = 0, v_2\le 0, x_1\ge 0, r\le \epsilon$ \\
        $\flow: \dot x_2 = 0, \dot v_2 = 0,$ \\
        $\dot x_1 = v_1, \dot v_1 = -g, \dot r = 1$ \\
        $\exit: r = \epsilon, r' = 0, v_2' = -c v_2$
      } (10);
      \path (00) edge (01);
      \path (01) edge (11);
      \path (-.1,1.9) edge[-] (.1,2.1);
      \path (3.9,1.9) edge[-] (4.1,2.1);
      \path (1.9, -.1) edge[-, double] (2.1,.1);
      \path (1.9, 3.9) edge[-, double] (2.1,4.1);
    \end{scope}
  \end{tikzpicture}
  \caption{%
    \label{fi:bouncing}
    Two independently bouncing balls}
\end{figure}

\begin{exmp}
  As a non-trivial example, we show a 2DHA which models two
  independently bouncing balls, following the \emph{temporal
    regularization} from~\citet{journals/scl/JohanssonELS99}, in
  Fig.~\ref{fi:bouncing}.  Here, the $2$-cube models the state in
  which both balls are in the air.  Its left and right edges are
  identified, as are its lower and upper edges, so that logically,
  this model is a torus.

  Its left / right edge is the state in which the second ball is in
  the air, whereas the first ball is in its $\epsilon$-regularized
  transition ($\epsilon> 0$) from falling to raising ($v_1' = -c v$,
  for some $c\in \mathopen] 0, 1\mathclose[$).  Similarly, its lower /
  upper edge is the state in which the first ball is in the air, while
  the second ball is $\epsilon$-transitioning.

  Due to the identifications, there is only one $0$-cube, which models
  the state in which both balls are $\epsilon$-transitioning; its
  $\inv$, $\flow$ and $\exit$ conditions can be inferred from the ones
  given.  With a notion of tensor product similar to the one for HDTA,
  this model can also be obtained as tensor product of the
  one-dimensional models for the individual balls.
\end{exmp}

\section{Conclusion}

We have seen that our new formalism of higher-dimensional timed
automata is useful for modeling interesting properties of
non-interleaving real-time systems, and that reachability for HDTA is
PSPACE-complete, but can be decided using zone-based algorithms.

We believe that our notion that in a non-interleaving real-time
setting, events should have a time duration, is quite natural.
Working on non-interleaving real-time semantics for Petri nets,
\citet{DBLP:conf/formats/ChatainJ13} remark that \textit{``[t]ime and
  causality [do] not necessarily blend well in [...] Petri nets''} and
propose to \emph{let time run backwards} to get nicer semantics.  We
should like to argue that our proposal of letting events have duration
appears more natural.

We have also seen how tensor product of HDTA can be used for parallel
composition, and that HDTA can easily be generalized to
higher-dimensional hybrid automata.  We believe that altogether, this
defines a powerful modeling formalism for non-interleaving real-time
systems.

redpajama_set_name: RedPajamaArXiv


Kett celebrates an Australian way of life; drawing inspiration from our natural landscapes and cosmopolitan cities.
Set amongst the green surrounds of the Abbotsford Convent, Kett is headed up by leading Australian designer Justin Hutchinson and his team. Collaborating with craftspeople from Australia, Italy and Indonesia to produce furniture with a timeless quality and technique.
As part of the inaugural release, Kett drew inspiration from the beautiful Victorian coastline.
In all, five new collections were presented, namely Addis, Aireys, Johanna, Otway and Wye. Each of the collections are defined by a specific colour, shape and form that is a representation of the Australian landscape from those regions.
A curated selection of fabrics, inspired by an Australian story.
Our story is a distillation of oceans, cities, mountains and deserts, complex in light, colour, texture and form, we have refined these elements.


text:
North America/
British Columbia & The Canadian Rockies
If you're searching for the promised land, there's a good chance you'll find it somewhere in the endless forests, inlet-punctuated coastline and meat-cleaver mountain ranges of Western Canada.
A Natural Show
Western Canada has historic sites, music venues and wonderful restaurants, but the real 'show' in these three provinces isn't hidden away in some dark, dusty museum; it's paraded outside in a dramatically expansive landscape of mountains, lakes, plains, forests, rocky bluffs and storm-lashed beaches. You haven't fully experienced this spectacular corner of the planet until you've gone for a swim in a glacier-fed lake, run with delight across an alpine meadow, followed in indigenous footsteps across a remote mountain pass, and watched a bear foraging for wild berries. Get in training!
Epic Adrenaline Rushes
Steely calved West Coasters have been discovering ways to interact with the outdoors for decades, and there are hundreds of operators here that can help you do the same. Whistler morphs from skiing capital to mountain-biking bonanza depending on the season. Banff and its satellite national parks contain an A-to-Z of trails, and Tofino is the original Canadian 'surf city'. Recent years have brought more creative inventions, including scarily long zip lines and numerous via ferrate (fixed-protection climbing routes). Alternatively, you can do what the First Nations have been doing for thousands of years and take to the water in a canoe or kayak.
Urban Adventures
It's easy to be seduced by the Canadian wilderness, but this region also offers sparkling city action. Alberta puts on a show with Edmonton's arts scene and Calgary's contemporary cowboy vibe, but it's British Columbia that offers the best city-based shenanigans, with two very different approaches. Provincial capital Victoria frames its increasingly cool scene with a backdrop of historic buildings, while Vancouver, Western Canada's largest city, provides a full menu of ethnically diverse neighborhoods that are ripe for exploration. From slick Yaletown to hipster-haven Main St, cool Gastown and the 'gayborhood' of West End, the 'City of Glass' is a place with many personalities.
Responsible for 95% of the region's history in a trajectory that stretches back over 10,000 years, Western Canada's indigenous culture – once rudely ignored, but now proudly exhibited – is part of a complex story of creation beliefs, against-the-odds survival and diverse First Nations traditions. Piecing it together will take you from the towering totems of Haida Gwaii to the chronicles of Vancouver's Museum of Anthropology. BC alone has 198 First Nations groups, nearly one-quarter of the Yukon's population claims indigenous heritage, while Alberta is the heartland of the Blackfoot and Cree. Uncover their legends in art galleries, cultural centers, festivals and hotels, or listen to their mythical stories retold in over 30 indigenous languages.
Jump to:Table of contents
Must see experiences
Featured & Latest stories
Must see in British Columbia & The Canadian Rockies
Stanley Park's Seawall Promenade
It sometimes takes awestruck visitors to remind Vancouverites they have Canada's finest urban park on their doorstep. But when you grow up alongside a 404-hectare temperate rainforest that's lined with multitudinous hiking and cycling trails, it's easy to think everyone is just as lucky. Stroll the park's 8.8km wave-licked, forest-backed seawall and you'll soon deplete your camera battery. But save some juice for the beady-eyed birdlife (especially the blue herons) around Lost Lagoon and a panoramic pyrotechnic sunset at Third Beach.
Must see in
Wildlife Spotting in Jasper
Elk nose their way around the town's edge, nervous deer dart between the trees and seemingly giant bald eagles swoop high overhead. The dramatic mountain setting of Jasper National Park is enough to keep most camera-wielding visitors content, but the surfeit of wandering wildlife makes you feel like you're part of a 3D nature documentary. If you're lucky you might even spot the show's stars: grizzly bears snuffling for berries alongside the highway or, across the other side of a river, wolves silently tracking their next fresh-catch ungulate.
Latest Stories from British Columbia & The Canadian Rockies
How to choose the best ski pass this winter
September 29th, 2020 • 5 min read
Ikon, Epic or Mountain Collective? Buy a multi-mountain ski pass and you'll get more time on the snow for less. Here's the run down for 2020-2021.
Experience First Nations traditions in British Columbia
September 8th, 2020 • 7 min read
There are 198 distinct First Nations in British Columbia, each with their own traditions and history – and visitors can experience this living history through cultural adventures.
Why British Columbia's Powder Highway is ideal for frosty family fun
Make this the year you begin a tradition of family travel with a trip to the Powder Highway in the Canadian Rockies.
A day out on the Vancouver SkyTrain
May 28th, 2019 • 5 min read
Metro Vancouver's 53-station SkyTrain network is one of Canada's most iconic transit services. But the three-line system – 79km of elevated and…
BC by sea: boating to the best of British Columbia
October 24th, 2018 • 7 min read
A large province in a large country, Canada's British Columbia is almost three times the size of Germany. So how do you begin to wrap your head around…
How to build a DIY rail and cruise tour of Canada and Alaska
A luxury rail journey combined with a coastal cruise is the hottest way to see western Canada and southeast Alaska. Each summer, thousands take a gourmet…
Where to find family adventure in the wintry Canadian Rockies
February 13th, 2017 • 6 min read
There might be no better time than winter to round up the kids and head to the Canadian Rocky Mountains for some unforgettable adventures. Pack plenty of…
These are our favorite local haunts, touristy spots, and hidden gems throughout British Columbia & The Canadian Rockies.
Discover more sights
Jasper is a rugged beauty; it's more raw and less tourist-pampering than its southern cousin Banff, and hence host to a more ambitious, adventurous visitor. Its tour de force is its extensive multipurpose trail network, much of it instantly accessible from the park's compact townsite. Backing it up is abundant wildlife, colossal icefields and–for the brave–the kind of desolate backcountry that makes you feel as though you're a good few miles (and centuries) from anything resembling civilization. Unlike Banff, most of Jasper's trails are multiuse, open to hikers, horseback riders and cyclists. Thanks to this liberal sharing policy, the park is able to offer the best network of off-road cycling trails in Canada–and they're not just for daredevils. Rated green (easy), blue (moderate) or black (difficult), they cater to pretty much everyone, including kids or parents with trailers in tow. An added bonus is that many of Jasper's trails start directly from the townsite, meaning you don't need to lug your bike around by car or bus. Using a special cycling trail map (free from the info office), numerous loops can be plotted from your hotel or campground, with time to incorporate hiking, swimming, canoeing or grabbing a cup of coffee along the way. Some of the most popular natural wonders, like Miette Hot Springs and Maligne Canyon, are easily accessible, and many more attractions are just a short hike away. Keep a little spare time in your itinerary to take advantage of the many diversions you stumble upon–a sparkling lake to admire, a snowshoe tour to explore or a moose to watch ambling by. As the largest of Canada's Rocky Mountain parks, Jasper will quickly captivate you with its beauty and serenity. Admission fees and other practicalities Jasper National Park and Banff National Park are connected by the Icefields Parkway –one of Canada's most famous road trips. There are three main road entrances to Jasper National Park. The East Park Entrance is on Hwy 16 between Jasper and Hinton, just east of Pocahontas. The West Park Entrance is on the same highway, 24km (15 miles) west of Jasper Town, near Yellowhead Pass and the border with British Columbia and Mt Robson Provincial Park. The Icefields Parkway Entrance is 6km south of Jasper Town on Hwy 93, on the way to Lake Louise. You must either buy or show a park pass at all entry gates. Park admission is C$10 for adults, C$8.70 for seniors, C$20 for families and free for kids under 17. There are additional fees for campground use, backcountry camping and fire permits. See the latest fees on the Jasper National Park website. Camping in Jasper National Park Three of Jasper's 10 campgrounds currently accept advance reservations: Wapiti, Wabasso and Pocahontas. Jasper's largest campground, Whistlers, is currently closed for renovation but will resume accepting reservations when it reopens in summer 2021. All other campgrounds operate on a first-come, first-served basis. Reservations are also recommended for backcountry camping, as Parks Canada limits the number of hikers on each trail. Both frontcountry and backcountry sites can be reserved via the Parks Canada website starting in late January each year. Jasper offers a handful of huts and lodges modeled on the European alpine tradition. All situated a good day's hike from the nearest road, these venerable backcountry retreats offer a unique wilderness experience without the hassle of setting up your tent or listening to things that go bump in the night. Hotels in Jasper National Park Aside from its venerable historic lodge, Jasper has a varied stash of hotels, motels, hostels, cabins, B&Bs and bungalows. Notwithstanding, in July and August you'd be wise to make reservations way in advance. Jasper gets seriously busy in July and August, and finding a room on the spur of the moment can be extremely difficult. Fortunately, aside from the standard clutch of hotels, motels and campgrounds, Jasper Town–which has a permanent population of 4500–has more than 100 B&Bs in private houses. The Jasper Home Accommodations Association maintains an excellent website of inspected B&Bs inside the park, complete with descriptions, contact details and web links. Prices range from C$75 to C$275 in high season and facilities often include kitchenettes, private entrances and cable TV. HI Jasper Patricia Lake Bungalows Mt Edith Cavell Wilderness Hostel Alpine Village Fairmont Jasper Park Lodge Tonquin Valley Backcountry Lodge
Why you should go Of all Canada 's top sights, Banff National Park justifiably ranks as many people's number one. As much a piece of history as a natural wonder, Canada's oldest national park, founded in 1885, is what Canada is all about. It's a feral, but largely accessible, wilderness that attempts to cater for everyone – and largely succeeds – from bus-tour visitors to hard-core mountaineers. The towering mountains of Banff provide endless opportunities for wildlife-watching, hiking, boating, climbing, mountain biking, or skiing. But you don't have to be a seasoned outdoor-enthusiast to enjoy Banff–its natural beauty will astound even those who just want to soak up the sights. Rugged canyons compete for your attention with fields of alpine wildflowers, turquoise lakes–like the famed Lake Louise and Moraine Lake –and dense emerald forests. One of the great beauties of Banff is its juxtaposition of the untamed and the civilized. Grizzly bears roam within growling distance of diners drinking cocktails at the romantic Banff Springs Hotel, while hikers fresh from summit attempts queue up for ice cream with golfers clutching nine irons. History Banff is a piece of history in itself. The region was home to First Nations peoples for 10,000 years before the creation of the park in 1885. Banff National Park is the world's third-oldest national park (and Canada's oldest). Cataloguing past triumphs and tribulations, Banff Town supports a healthy cache of four museums, virtually unparalleled for a 'natural' national park. Tickets and other practicalities Park admission is C$10 for adults, C$8.70 for seniors, C$20 for families and free for kids under 17. There are additional fees for campground use, backcountry camping, fire permits and fishing permits. See the latest fees on the Banff National Park website. Camping in Banff National Park Banff has 14 frontcountry campgrounds catering for tents, recreational vehicles (RVs) and camper vans. Most are open from around June to mid-September, although Tunnel Mountain Village Two and Lake Louise Trailer campgrounds are open year-round. Advance reservations are available for Tunnel Mountain, Two Jack, Johnston Canyon, Lake Louise and some sites at Rampart Creek. The Parks Canada website starts taking reservations in January each year for a fee of C$11 in addition to regular camping fees. Book as far ahead as possible, as sites fill up fast. Sites at all other campgrounds are allocated on a first-come, first-served basis, so the best way to claim a spot is to turn up early (around the official 11am checkout time is best) or check with parks staff about which campgrounds currently have availability. Banff Park Radio (101.1FM) also releases regular bulletins on campgrounds with available sites. It's a good idea to stay in one place over weekends; sites are generally easier to come by midweek. There's a maximum stay of 14 nights and a maximum occupancy of six people per site. At larger campgrounds you can pay fees at the entry kiosk, but at smaller campgrounds, you'll have to self-register: find a vacant site first, then go to the self-registration shelter, remembering to enter your name, site number, license plate and duration of stay on the envelope along with the relevant fees. If it's late when you arrive, you can do this in the morning, or sometimes staff will come around and collect your fees in person in the morning. Fires are usually allowed at campsites where there's a fire pit – you'll need to buy a fire permit (C$8.80, including wood) from the campground entrance. Watch for fire restrictions during dry periods. Hotels in Banff National Park Despite having enough hotel rooms to rival a town three times its size, finding a place to sleep in Banff Town can be tricky. Demand is huge, and rates are notoriously expensive, especially in peak season. Many visitors choose to cut costs by camping, hosteling, hiring recreation vehicles or staying in nearby Canmore. Regardless of where you stay, book well ahead, especially if you're coming in June, July or August. Skoki Lodge Fairmont Banff Springs Buffaloberry Paradise Lodge & Bungalows Banff Log Cabin B&B
One of North America's largest urban green spaces, Stanley Park is revered for its dramatic forest-and-mountain oceanfront views. But there's more to this 400-hectare woodland than looks. The park is studded with nature-hugging trails, family-friendly attractions, sunset-loving beaches and tasty places to eat. Why you should go Built in stages between 1917 and 1980, the park's 8.8km seawall trail is Vancouver 's favorite outdoor hangout. Encircling the park, it offers spectacular waterfront vistas on one side and dense forest on the other. You can walk the whole thing in roughly three hours or rent a bike to cover the route far faster. Keep in mind: cyclists and in-line skaters must travel counterclockwise on the seawall, so there's no going back once you start (unless you walk). Also consider following the 25km of trails that crisscross the park's interior, including Siwash Rock Trail, Rawlings Trail and the popular Beaver Lake Trail (some routes are for pedestrians only). The Beaver Lake route is especially recommended; a family of beavers resides there and you'll likely spot them swimming around their large den. The seawall also delivers you to some of the park's top highlights. About 1.5km from the W Georgia St entrance, you'll come to the ever-popular totem poles. Remnants of an abandoned 1930s plan to create a First Nations 'theme village,' the bright-painted poles were joined by some exquisitely carved Coast Salish welcome arches a few years back. For the full First Nations story, consider a fascinating guided park walk with Talaysay Tours. Continue on to the nearby Nine O'Clock Gun (it fires at 9pm nightly) and Lumberman's Arch, which is a good spot to see Alaska cruise ships sliding past. From here, you can cut into the park to the popular Vancouver Aquarium or continue around the seawall; it gets wilder and more scenic as you pass under the Lions Gate Bridge and face down the Pacific Ocean. Wildlife in Stanley Park Stanley Park is studded with appeal for wildlife fans. Neat the W Georgia St entrance lies Lost Lagoon, which is a bird-beloved nature sanctuary – keep your eyes peeled for blue herons. Its perimeter pathway is also a favored stroll for wildlife nuts. Plunging deeper into the park's more secluded trails, you'll also likely spot wrens, hummingbirds and chittering little Douglas squirrels. For an introduction to the area's flora and fauna, start at the Stanley Park Nature House. You'll find friendly volunteers and exhibits on wildlife, history and ecology – ask about their well-priced guided walks. While they mostly give humans a wide berth, you might also come across a coyote or two; aggressive incidents with coyotes are rare. However, be cautious and treat them with respect and give them a wide berth as well. Beaches in Stanley Park Second Beach is a family-friendly area on the park's western side, with a grassy playground, an ice-cream-serving concession and a huge outdoor swimming pool. It's also close to Ceperley Meadows, where Fresh Air Cinema offers popular free outdoor movie screenings in summer. For a little more tranquility, try Third Beach. A sandy expanse with plenty of logs to sit against, this is a favored summer-evening destination for Vancouverites. Opening hours and other practicalities The park is free to enter and open 24 hours a day. The park can be reached by taking bus 19 from downtown. There are additional fees for bike rentals and attractions in the park, like the Vancouver Aquarium. In summer, the seawall is packed with visitors; arrive early morning or early evening if tranquil nature-communing is your bag. There are often summertime queues to enter the aquarium; try to make it one of your first stops when you arrive at the park. Hotels near Stanley Park Buchan Hotel Times Square Suites Hotel Sylvia Hotel
Why you should go Considered by many to be the crown jewel of Banff National Park, Lake Louise is nearly impossible to describe without resorting to clichés. This implausibly turquoise lake is ringed by chiseled mountains capped by Victoria Glacier. Roughly 2km (1.2 miles) end to end and 70m (230ft) deep, the lake is famous for its stunning blue water, caused by light reflecting off tiny particles of 'rock flour' (glacial silt) carried down from the mountain glaciers. The lake has become one of Banff National Park's most famous (and busiest) attractions, and the lakeshore inevitably gets crowded on summer days. Visit as early as possible to avoid the squash, and spend the rest of the day exploring the nearby attractions of Moraine Lake and the Lake Louise Gondola. You can usually escape the coachloads of sightseers milling around in front of the Fairmont Chateau Lake Louise by following the lakeshore trail, which tracks through forest along the northern side of the lake, offering fabulous vistas of Fairview Mountain and the Victoria Glacier. A spur trail leads steeply up the mountainside to the famous Lake Agnes Teahouse and the Big Beehive lookout, but it's a long slog, so you'll need good shoes and plenty of water. Further along the lakeshore trail, you can continue up the valley on the Plain of Six Glaciers walk. There are several more classic hikes leading off around Lake Louise, including the steep climbs up Saddleback (2330m/7644ft) and Fairview Mountain (2744m/9003ft), which both brood along the lake's southern shore. For something more sedentary, you can hire canoes from the Lake Louise Boathouse. Once you've got over the shock of the price, you'll be rewarded with a sense of the silence and natural majesty. Tickets and other practicalities Banff National Park admission is C$10 for adults, C$8.70 for seniors, C$20 for families and free for kids under 17. There are additional fees for campground use, backcountry camping, fire permits and fishing permits. See the latest fees on the Banff National Park website. There is a C$11.70 fee per vehicle for parking at the Lake Louise lakeshore. Lake Louise is best seen early or late in the day, when the vibrant colors of the lake are strongest. In winter the scene is transformed into a wonderland of powder-white ice. As it freezes over its signature blue waters won't be visible–but it does become an epic skating rink. Lake Louise 'village,' just off Trans-Canada Hwy/Hwy 1, is little more than an outdoor shopping mall, a gas station and a handful of hotels. Hotels near Lake Louise Other than a very popular hostel and a fantastic riverside campground, Lake Louise doesn't have much in the way of budget accommodations. At the pricier end of the spectrum you'll find some truly splurge-worthy properties, including cabins, historic lodges and one of the Canadian Rockies' most iconic lakeside hotels, the opulent Fairmont Chateau Lake Louise.
Why you should go The spectacular, deep teal waters of Moraine Lake are one of Banff National Park's most iconic sights. The lake's rugged and remote setting in the Valley of the Ten Peaks, accessed via a narrow winding road, only add to its allure, Many visitors actually prefer Moraine Lake to the more famous Lake Louise –so many, in fact, that you'll have to be lucky or an early riser to get a parking spot here; the lot often fills up by 5:30am in peak season. At the eastern end of the lake is the Moraine Lake Rockpile, a massive heap of boulders of somewhat uncertain origin: some geologists think it was created by an ancient avalanche, while others believe it was formed by the long-gone glacier that carved out the rest of the valley. A paved trail leads up to a series of viewpoints at the top of the rockpile, offering a panoramic vista across the lake and the Wenkchemna Peaks beyond. A part-paved trail leads off around the lake's northern shore, linking up with the branch trail to Larch Valley and Eiffel Lake. Another trail leads southeast from the rockpile to Consolation Lakes. Alternatively, you can explore the lake in the manner of the old voyageurs by hiring a canoe from the boathouse next to Moraine Lake Lodge. Tickets and other practicalities Banff National Park admission is C$10 for adults, C$8.70 for seniors, C$20 for families and free for kids under 17. There are additional fees for campground use, backcountry camping, fire permits and fishing permits. See the latest fees on the Banff National Park website. The Moraine Lake Road closes seasonally–from about October to May–due to the avalanche risk.
Encompassing 11,228 sq km of Rocky Mountains wilderness, including jagged peaks, vast forests, glacial lakes and the magnificent Columbia Icefield, Jasper shelters some of the most pristine natural features on the North American continent. Jasper receives over two million visitors annually, making it Canada's second most popular national park.
To be accurate, this 1350-sq-km park should be called '430 Glaciers National Park'. The annual snowfall can be as much as 23m, and due to the sheer mountain slopes, this is one of the world's most active avalanche areas. For this reason, skiing, caving and mountaineering are regulated; you must register with park wardens before venturing into the backcountry. Check the weather and get an avalanche report. Rogers Pass ranks as one of the world's most beautiful mountain passes. Be sure to pause at the Hemlock Grove Trail, 54km east of Revelstoke, where a 400m boardwalk winds through an ancient hemlock rainforest.
Gwaii Haanas National Park Reserve, National Marine Conservation Area Reserve & Haida Heritage Site
This huge Unesco World Heritage site encompasses Moresby and 137 smaller islands at its southern end. It combines a time-capsule look at abandoned Haida villages with hot springs, amazing natural beauty and some of the continents best kayaking. A visit demands advance planning as the number of visitors entering the park each day is limited. The easiest way is to take a guided trip with a licensed operator; access to the park is by boat or floatplane only.
Royal Tyrrell Museum of Palaeontology
This fantastic museum is one of the pre-eminent dinosaur museums on the planet, made even better by a $5.9 million expansion project completed in 2019. Even if you have no interest in dinos, you'll come out feeling like you missed your calling as a paleontologist. The exhibits are nothing short of mind-blowing. Unlike some other dinosaur exhibits, there's nothing dusty or musty about this super-modern place. Children will love the interactive displays.
More sights
Top experiences
Whether it's a guided tour of a historic landmark, private tasting of local delicacies, or an off-road adventure — explore the best experiences in British Columbia & The Canadian Rockies.
Discover more activities
Half-Day Whale Watching Adventure from Vancouver
Victoria Guided Food and History Tour
Whistler ATV Bushwacker Tour
Vancouver Highlights Bike Tour - The Grand Tour
Zipline Adventure in Whistler
Half-Day Whale Watching Adventure from Victoria
Okanagan Flyboard Experience Kelowna
Whistler Odyssey Tour: Off-Road Buggy Adventure
Vancouver Lost Souls of Gastown Walking Tour
Wet and Wild Elaho Exhilarator Rafting
The Forbidden Downtown and Gastown Walking Tour
Banff Gondola Ride Admission
Johnston Canyon Icewalk
Whistler Wilderness Run Snowmobile Tour
Rafting Adventure on the Kicking Horse River
Riverside Rafting on Clearwater River in Wells Gray Park
Wake up with breakfast poutine in Calgary
For Explorers Everywhere
Get 20% off our online shop.
I want emails from Lonely Planet with travel and product information, promotions, advertisements, third-party offers, and surveys. I can unsubscribe any time using the unsubscribe link at the end of all emails. Contact Lonely Planet or view our Privacy Policy.

redpajama_set_name: RedPajamaCommonCrawl


Made from the same material as Loulou Lollipop's signature swaddle, your little one will love how soft the luxury muslin fitted sheet feels. These sheets make a great newborn gift package!
Made from 30/70 blend of cotton and bamboo rayon.
Size 28' x 52' x 9'.
Wash in cold water only.


Dashcam shows cops fighting – Bergen County Police vs NJ State. This video provides America with the evidence as to what kind of people we're giving guns and badges to. While one officer is no better than the other, the unprofessional language and actions speak loud and clear. The fact that the name of the problem trooper was redacted shows total guilt by the department. Body language also tells the public about the mentally unstable officer. Its not about being careful or cautious its about HOW he did this, the instant anger, abusive language and then not being able to back down after he was found to be wrong about his suspicions. Attitude, Ego and quick to anger are ingredients for disaster.
The two Bergen County Police Department officers who were caught on video having a heated argument with a state trooper in May were disciplined following the incident.
If the use of language and posturing is NORMAL then we would expect a response such as above, however the Chief seems to miss the entire point of the public being in danger having officers with such short fuses being in possession of firearms. The American public deserves a higher quality officer and attitude without the major ego issues. The response by the chief shows how the problem ultimately is at the top of the food chain. There was an obvious Ego battle battle going on which quickly got out of control, at what point do we have to get involved, when one officer fires a weapon?
This brings up another issue which is privacy, if the public has no right to privacy than why do these officers have that right?
This needs to be changed and the public who pay these officers have the right to know what is done for their money. The officers and the department have no right to do this, in fact its only a way to cover up a crime and pretend to punish when in fact we'll never know the truth. This is a public service not a top secret clearance agency.
acting. Now think about this, if a police officer does not trust the unmarked police vehicle WHY should any citizen stop for one? Are citizens suppose to take chances even with their own firearm? Its this two sided thinking, double standards and lack of respect for the public which has destroyed the public's image of police in general.


your chrome hearts handbags,your online store,clothing: Sitting on the 120G goddess model car is what kind of experience?
Sitting on the 120G goddess model car is what kind of experience?
but also possession of dry cargo!!! Down down down down down: it is said that there is such a goddess! By: is this a few car vision Zhang also did not look fun real welfare here 120G beautiful SkyDrive down down down the reply: chemo view the goddess.


There are several types of fractures that you can carry your windscreen. One of the most typical ones are Bull's eye, chip, mix break, fracture chip, ding, edge crack, advance fracture, half moon, lengthy fracture, partial bull's eye, pit, celebrity break, tension fractures, as well as stone break.
I recognize these terms might be extremely unknown, so I have included some illustrations to assist you imagine the usual types. Name don't matter that much. You could fix practically any kind of sort of split nowadays.
A few years earlier, the tools utilized for fixing windshield just weren't made public. If you are a rather technical person, or have a passion for discovering brand-new points, you could most definitely make use of these tools with ease.
If you have a little chip or split on your windshield; don't postpone the repair service. All long cracks begin with these smaller sized ones. Gradually, they just maintain getting longer as well as longer up until the glass shatters completely.
These smaller ones are extremely easy to fix as well as cost just 10-20 bucks. They are several high quality windshield repair work sets for tiny cracks that you can get.
Determining if you need windshield substitute or repair work, windscreen replacement cost as well as navigating your insurance plan could add to the stress of your situation. The price of windshield repair work or replacement can be in between $10 and $470 for the ordinary vehicle owner, but several aspects play a part in the price.
Small chips as well as tiny fractures in an automobile's windscreen could be qualified for windscreen repair work. Repair works are typically small issues as well as not in the driver's straight view. If you are unsure if a windscreen replacement or repair is required, a certified service technician at your neighborhood car service center can identify so repair is required.
Some individuals could not understand that windscreen repair service cost is usually fully covered by their insurance coverage. Numerous vehicle insurance provider cover windshield repair services in full, without insurance deductible, to prevent expensive substitutes.


I'm headed for China for two weeks! I will have internet and plan to "work," but if there is a slight delay in answering emails, etc., that's why!
My grandson Ethan turned one last month, and I'm working on making him a little book. I'm getting it printed through Pint Size Productions, a great printing company in New York that offers Print-On-Demand printing, so I can order just one if I like.
I'm delighted to announce a new teacher in our lineup, Seattle artist Fred Lisaius!
This 6-Lesson online class runs over a two-week period starting May 19th. $85. Click HERE for more information and to sign up!
I've had plenty of them the past few days!
Here are some really GOOD things, though!
1. Tomorrow I am opening registration for a new watercolor class by Seattle artist Fred Lisaius. Just look at one of his wonderful paintings!
Steve and I met Fred a few months ago and what a delightful human he is! The above is an acrylic painting, which he will teach later in the year, but his watercolors are just as lovely.
3. Our son Wes got a role in the St. John's College production of "King Lear," which will be performed this coming weekend. We are going to Maryland to see Wes play Edgar, the "good" son, because how often does your kid win a lead role in a Shakespeare play?
One fun thing about moving house is that you run across all kinds of things you had forgotten about. Here are three experiments/drawings that I did about four years ago I think.
This turtle was drawn from life at the Woodland Park Zoo here in Seattle while taking a class from Barbara Fulgate.
A reminder that the DRAW! 21-Day class begins today! Join me if you can!
Registration Now Open for Encaustics Class!
On Monday-Wednesday-Friday of each session you will receive an email reminding you to visit the class blog for your new assignment and video lesson. Videos are professionally produced and instructor feedback will be given via a private facebook page (or via email with Stephanie, if you prefer). If you need to miss a week, don't worry! The class material will be up and available to you for one year from the date of purchase.
FOR MORE DETAILS AND TO SIGN UP, CLICK HERE!
Also, Stephanie is offering her hand-mixed beeswax for sale. Cool! See details HERE.
If you've ever been curious about encaustic painting, watch this delightful talk with Seattle artist Stephanie Hargrave!
I think this elephant is definitely afraid of that mouse!
But experiments in the studio must go on!
A detail of the above; PanPastel + acrylic paints.


The 2018 Great Maker Search: Jewelry Edition is now open for voting. We encourage you to show your support for your fellow crafter entries and help us share with others. Anyone can vote, and you can cast one vote per entry per day.
This round will run until March 30th at 11:59PM. The Winner will be announced and prizes awarded on April 2nd.
Thank you for supporting handmade and the Great Maker Search presented by ArtFire!
Thanks for the heads up! Voting!


text:
The football competition at the 2013 Francophone Games is a tournament open to under 20 age group national teams.

Participants

 (invitee) -withdrew
 - withdrew

 (invitee)

Matches

Group stage

Group A

Group B

Group C

Group D

Knockout stage

Semifinals

Third place playoff

Final

Squads

Burkina Faso

Canada

Republic of the Congo

Ivory Coast

Cameroon

Democratic Republic of the Congo

France

Gabon

Haiti

Lebanon
Source:

Morocco

Niger

Rwanda

Senegal

Source:

References

football
2013
2013 in African football
2013
2013–14 in Moroccan football
2013–14 in French football
2013 in Canadian soccer
2013 in Cameroonian football
2013–14 in Lebanese football
2013–14 in Ivorian football


text:
Historians Find Adolf Hitler's Vegetable Garden at Ruins of His Secret Headquarters - Reports
© AP Photo / Czarek Sokolowski
07:31 15.11.2019 Get short URL
https://sputniknews.com/viral/201911151077311060-historians-find-adolf-hitlers-vegetable-garden/
A garden that once provided Adolf Hitler with fresh vegetables has been discovered at his infamous Wolf's Lair headquarters in Poland, where the Nazi leader spent most of the final years of the war.
The top-secret, heavily guarded bunker complex on the grounds of Mazurolandia was used by the Nazis until January 1945, when it was abandoned and partly destroyed ahead of advancing Soviet forces. The excavations took place during the summer when the garden was found.
"We discovered Hitler's Garden in the 4th Zone of the Wolf's Lair," said Mazurolandia park, in a translated statement, adding that experts from the Mazurian Military Museum were brought in to investigate the site.
The First News reports that the garden was found 2,953 feet from Hitler's bunker. The excavation uncovered the foundations of the gardener's house, two greenhouses and an underground boiler room that provided water and warm air to grow fresh produce all year round. Wartime ceramics, porcelain and glassware confirmed the time the garden was operational.
Gardens and greenhouse complex are discovered at Adolf Hitler's Wolf's Lair bunker https://t.co/eOwoicPUqj pic.twitter.com/IwOOFZL4TW
— Week Facts (@WeekFacts) November 14, 2019
Hitler was a vegetarian, teetotaler and non-smoker, so his bunker had vegetables delivered on a regular basis. Later in life, he was paranoid about being poisoned, so the Nazi leader also ensured that a number of food tasters worked at the Wolf's Lair to sample his meals.
"The food was delicious, only the best vegetables, asparagus, bell peppers, everything you can imagine. And always with a side of rice or pasta," Margot Woelk, one of the food tasters, told the Associated Press in 2013.
Woelk, then in her mid-twenties, spent almost 22 years as one of 15 young women who sampled Hitler's food at the Wolf's Lair.
The Wolf's Lair was also the scene of an unsuccessful attempt to assassinate the evil German leader on July 20, 1944, when trusted colonel Claus von Stauffenberg detonated a bomb in a conference room at the headquarters. Hitler survived, but nearly 5,000 people were executed following the assassination attempt, including von Stauffenberg.
A number of Nazi sites from World War II have been unearthed in recent years. Earlier this year, local government officials announced the discovery of hundreds of items at Nazi massacre sites in northwestern Germany. Experts are also looking to unlock the sinister secrets of hidden Nazi bases dotted across Europe, including the vast base of Dag Bromberg, which, like the Wolf's Lair, is hidden in a Polish forest, and the V-2 rocket base Kraftwerk Nord West in France.
How 8 November Could've Changed History and Saved the World from Adolf Hitler?
Utah Teacher Suspended After Student Dresses as Hitler for Halloween - Reports
German Diplomat Voices Shock After Seeing Hitler Mask in Prague
Hitler's 'Brainchild': The History of the Iconic Volkswagen Beetle
history, Nazi, Adolf Hitler, Poland