Automata for true concurrency properties